Security hardening, modern CSS redesign, and verified CSP builder.

Authorfritjof@alokat.org
Date2026-04-14 10:00:59
Hash5f529afaada2f013be22cec4413abd8d2380798d

Summary

A ./.dockerignore
A ./Caddyfile
A ./Dockerfile
M ./README.md +100
A ./Setup.hs
A ./app/
A ./app/Main.hs
M ./darcsweb.cabal +3
A ./docker-compose.yml
A ./nginx.conf
M ./src/DarcsWeb/Darcs.hs -4 +19
A ./static/darcs-logo.png
M ./static/style.css -174 +598
A ./test/
A ./test/Properties/
A ./test/Properties/Csp.hs
A ./test/Properties/Html.hs
A ./test/Spec.hs
A ./verified/
A ./verified/Makefile
A ./verified/csp_pure.v
A ./verified/csp_pure_proofs.v
A ./verified/html_pure.v
A ./verified/html_pure_proofs.v
A ./verified/path_pure.v
A ./verified/path_pure_proofs.v

Diff

patch 5f529afaada2f013be22cec4413abd8d2380798d
Author: fritjof@alokat.org
Date:   Tue Apr 14 10:00:59 UTC 2026
  * Security hardening, modern CSS redesign, and verified CSP builder.
addfile ./.dockerignore
hunk ./.dockerignore 1
+.stack-work/
+_darcs/
+.claude/
+*.vo
+*.vok
+*.vos
+*.glob
+.*.aux
addfile ./Caddyfile
hunk ./Caddyfile 1
+# Caddy reverse proxy for DarcsWeb
+#
+# Caddy automatically provisions and renews TLS certificates via ACME (Let's
+# Encrypt) and enables HSTS by default.  This configuration adds additional
+# security hardening on top.
+#
+# Usage:
+#   caddy run --config Caddyfile
+#
+# Or with docker compose (replace the nginx service):
+#   caddy:
+#     image: caddy:2-alpine
+#     ports: ["80:80", "443:443", "443:443/udp"]
+#     volumes:
+#       - ./Caddyfile:/etc/caddy/Caddyfile:ro
+#       - caddy_data:/data
+#       - caddy_config:/config
+
+darcs.example.com {
+	# Rate limiting: 10 requests/s per client IP, burst of 20
+	rate_limit {
+		zone darcsweb {
+			key    {remote_host}
+			events 10
+			window 1s
+		}
+	}
+
+	# Security headers (layered with application-level headers)
+	header {
+		# Prevent MIME type sniffing
+		X-Content-Type-Options "nosniff"
+		# Prevent clickjacking
+		X-Frame-Options "DENY"
+		# Control referrer information
+		Referrer-Policy "strict-origin-when-cross-origin"
+		# Restrict browser APIs
+		Permissions-Policy "camera=(), microphone=(), geolocation=(), payment=()"
+		# Prevent search engine indexing
+		X-Robots-Tag "noindex, nofollow"
+		# Remove server identification
+		-Server
+	}
+
+	# Reverse proxy to darcsweb backend
+	reverse_proxy darcsweb:3000 {
+		# Timeouts to prevent slow-loris and idle connections
+		transport http {
+			dial_timeout      5s
+			response_header_timeout 30s
+		}
+
+		# Pass client info to backend
+		header_up X-Real-IP {remote_host}
+		header_up X-Forwarded-Proto {scheme}
+	}
+
+	# Limit request body size (read-only app, no uploads expected)
+	request_body {
+		max_size 4KB
+	}
+
+	# Access log
+	log {
+		output file /var/log/caddy/darcsweb.log {
+			roll_size 10MiB
+			roll_keep 5
+		}
+	}
+}
addfile ./Dockerfile
hunk ./Dockerfile 1
+# syntax=docker/dockerfile:1
+# -- Build stage --
+#
+# The haskell and debian base images are multi-arch (amd64 + arm64), so this
+# Dockerfile works natively on x86-64 as well as ARM64 hosts like the
+# Raspberry Pi 5.  Building on the Pi itself is slow; see README.md for
+# cross-build instructions.
+
+FROM haskell:9.6-slim AS build
+
+# Install Rocq (needed for verified extraction) and build tools
+RUN apt-get update && \
+    apt-get install -y --no-install-recommends \
+      opam make sed ca-certificates \
+      libgmp-dev linux-libc-dev pkg-config && \
+    rm -rf /var/lib/apt/lists/*
+
+# Pin OCaml compiler and Rocq versions for reproducible builds
+RUN opam init --disable-sandboxing --bare -y && \
+    opam switch create default ocaml-base-compiler.4.14.2 && \
+    eval $(opam env --switch=default) && \
+    opam pin add rocq-core 9.0.0 -n && \
+    opam pin add rocq-stdlib 9.0.0 -n && \
+    opam install rocq-core.9.0.0 rocq-stdlib.9.0.0 -y
+
+WORKDIR /src
+
+# Copy dependency manifests first to cache the resolver/GHC download
+COPY stack.yaml stack.yaml.lock darcsweb.cabal Setup.hs LICENSE ./
+RUN eval $(opam env --switch=default) && \
+    stack setup --install-ghc --no-terminal
+
+# Copy sources and build
+COPY src/ src/
+COPY app/ app/
+COPY test/ test/
+COPY verified/ verified/
+COPY gen/ gen/
+
+RUN eval $(opam env --switch=default) && \
+    stack build --install-ghc --no-terminal --copy-bins --local-bin-path /usr/local/bin
+
+# -- Runtime stage --
+FROM debian:bookworm-slim
+
+RUN apt-get update && \
+    apt-get install -y --no-install-recommends libgmp10 && \
+    rm -rf /var/lib/apt/lists/* && \
+    groupadd -r darcsweb && \
+    useradd -r -g darcsweb -s /sbin/nologin darcsweb
+
+COPY --from=build /usr/local/bin/darcsweb /usr/local/bin/darcsweb
+COPY static/ /usr/share/darcsweb/static/
+
+COPY <<'EOF' /etc/darcsweb.conf
+bind = 0.0.0.0
+port = 3000
+repos = /srv/darcs
+title = DarcsWeb
+static = /usr/share/darcsweb/static
+EOF
+
+USER darcsweb
+EXPOSE 3000
+ENTRYPOINT ["darcsweb", "-c", "/etc/darcsweb.conf"]
hunk ./README.md 158
+### Docker
+
+The included `Dockerfile` produces a minimal image with just the `darcsweb`
+binary and static assets. The base images (`haskell:9.6-slim`,
+`debian:bookworm-slim`) are multi-arch, so this works on both x86-64 and ARM64
+hosts such as the Raspberry Pi 5.
+
+Build the image:
+
+```
+docker build -t darcsweb .
+```
+
+Run it, bind-mounting your host repositories read-only:
+
+```
+docker run -d -p 3000:3000 -v /srv/darcs:/srv/darcs:ro darcsweb
+```
+
+The `:ro` mount is sufficient -- DarcsWeb only reads `_darcs/` contents. Because
+bind mounts reflect the host filesystem in real time, new patches and new
+repositories show up immediately without restarting the container.
+
+To override the built-in configuration, mount your own file:
+
+```
+docker run -d -p 8080:8080 \
+  -v /srv/darcs:/srv/darcs:ro \
+  -v /etc/darcsweb.conf:/etc/darcsweb.conf:ro \
+  darcsweb
+```
+
+Multiple repository directories can be served by mounting them under a common
+prefix:
+
+```
+docker run -d -p 3000:3000 \
+  -v /home/user/repos:/srv/darcs/personal:ro \
+  -v /srv/shared:/srv/darcs/shared:ro \
+  darcsweb
+```
+
+#### Cross-building for Raspberry Pi 5
+
+If you prefer to build the image on a faster x86-64 machine and deploy to
+a Pi 5:
+
+```
+docker buildx build --platform linux/arm64 -t darcsweb:arm64 --load .
+docker save darcsweb:arm64 | ssh pi@raspberrypi docker load
+```
+
+This requires Docker Buildx with QEMU emulation (`docker run --privileged
+--rm tonistiigi/binfmt --install arm64`).
+
+#### TLS with Let's Encrypt
+
+The included `docker-compose.yml` and `nginx.conf` add an nginx reverse proxy
+with automatic Let's Encrypt certificates via certbot.
+
+1. Replace `darcs.example.com` with your domain in both `nginx.conf` and the
+   certbot command below.
+2. If your repositories are not in `/srv/darcs`, update the volume mount in
+   `docker-compose.yml`.
+3. Start nginx and darcsweb (certbot needs nginx running for the ACME
+   challenge):
+
+```
+docker compose up -d nginx darcsweb
+```
+
+4. Obtain the initial certificate:
+
+```
+docker compose run --rm certbot certonly --webroot \
+  -w /var/www/certbot -d darcs.example.com
+```
+
+5. Reload nginx to pick up the new certificate, then start the certbot
+   renewal sidecar:
+
+```
+docker compose exec nginx nginx -s reload
+docker compose up -d certbot
+```
+
+The certbot container renews certificates automatically every 12 hours (a
+no-op when they are not yet due). After renewal nginx must be reloaded; a
+cron entry on the host handles this:
+
+```
+0 */12 * * * docker compose exec nginx nginx -s reload
+```
+
+Certificate data is stored in the `certbot_conf` volume and persists across
+restarts.
+
hunk ./README.md 281
+| `build_csp` / `sanitize_value` | `verified/csp_pure.v` | CSP header construction in `Main` |
hunk ./README.md 296
+- **CSP injection safety**: `sanitize_value` strips all semicolons, proven by
+  structural induction -- prevents injecting new CSP directives via values.
addfile ./Setup.hs
hunk ./Setup.hs 1
+import Distribution.Simple
+import Distribution.Simple.UserHooks (UserHooks(..))
+import System.Process (callCommand)
+
+main :: IO ()
+main = defaultMainWithHooks simpleUserHooks
+  { preBuild = \args flags -> do
+      callCommand "make -C verified extract"
+      preBuild simpleUserHooks args flags
+  }
adddir ./app
addfile ./app/Main.hs
hunk ./app/Main.hs 1
+{-# LANGUAGE ForeignFunctionInterface #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Main (main) where
+
+import           Web.Scotty (scottyOpts, ScottyM, ActionM, get, notFound,
+                             pathParam, html, status, liftIO,
+                             Options(..), defaultOptions, file, setHeader,
+                             request, regex, middleware)
+import           Network.Wai.Handler.Warp (setPort, setHost, defaultSettings)
+import           Network.HTTP.Types.Status (status404, status403)
+import           Network.Wai (pathInfo, modifyResponse, mapResponseHeaders,
+                             Middleware)
+import           Data.String (fromString)
+
+import qualified Data.ByteString.Char8 as BC
+import qualified Data.Text as T
+import qualified Data.Text.Lazy as TL
+import           Data.Time.Clock (getCurrentTime)
+import           System.Console.GetOpt
+import           System.Environment (getArgs, getProgName)
+import           System.Directory (makeAbsolute, canonicalizePath,
+                                   doesFileExist)
+import           System.FilePath ((</>), takeExtension)
+import           System.Exit (exitFailure, exitSuccess)
+import           System.IO (hPutStrLn, stderr, hFlush, stdout)
+import           System.Posix.Process (forkProcess, createSession)
+import           System.Posix.IO (dupTo, stdInput, stdOutput, stdError)
+import           System.Posix.Syslog (withSyslog, syslog, Facility(..),
+                                      Priority(..), Option(..))
+import           Foreign.C.String (withCStringLen, withCString, CString)
+import           Foreign.C.Types (CInt(..))
+import           System.Posix.Types (Fd(..))
+import           Data.List (isPrefixOf)
+
+import           DarcsWeb.Types
+import           DarcsWeb.Config
+import           DarcsWeb.Darcs
+import           DarcsWeb.Html
+import qualified PathPure
+import qualified CspPure
+
+-- Command-line options
+data Opts = Opts
+  { optConfigFile :: Maybe FilePath
+  , optDaemon     :: Bool
+  } deriving (Show)
+
+defaultOpts :: Opts
+defaultOpts = Opts
+  { optConfigFile = Nothing
+  , optDaemon     = False
+  }
+
+optDescr :: [OptDescr (Opts -> Opts)]
+optDescr =
+  [ Option "c" ["config"]
+      (ReqArg (\f o -> o { optConfigFile = Just f }) "FILE")
+      "configuration file (required)"
+  , Option "d" ["daemon"]
+      (NoArg (\o -> o { optDaemon = True }))
+      "run as daemon (log to syslog)"
+  ]
+
+parseOpts :: [String] -> IO Opts
+parseOpts argv =
+    case getOpt Permute optDescr argv of
+      (o, _, [])   -> return (foldl (flip id) defaultOpts o)
+      (_, _, errs) -> do
+        hPutStrLn stderr (concat errs)
+        usage
+
+usage :: IO a
+usage = do
+    prog <- getProgName
+    hPutStrLn stderr (usageInfo ("Usage: " ++ prog ++ " -c FILE [-d]") optDescr)
+    exitFailure
+
+main :: IO ()
+main = do
+    args <- getArgs
+    opts <- parseOpts args
+
+    configPath <- case optConfigFile opts of
+      Nothing -> usage
+      Just f  -> return f
+
+    cfgMap <- parseConfigFile configPath
+
+    let port      = read (cfgLookupDefault "port" "3000" cfgMap)
+        bind      = cfgLookupDefault "bind" "127.0.0.1" cfgMap
+        repoDir   = cfgLookupDefault "repos" "." cfgMap
+        title     = T.pack (cfgLookupDefault "title" "DarcsWeb" cfgMap)
+        staticDir = cfgLookupDefault "static" "static" cfgMap
+
+    absRepoDir   <- makeAbsolute repoDir >>= canonicalizePath
+    absStaticDir <- makeAbsolute staticDir >>= canonicalizePath
+
+    if optDaemon opts
+      then do
+        logStdout $ "Daemonizing (bind " ++ bind ++ ":" ++ show port ++ ")"
+        hFlush stdout
+        daemonize $ withSyslog "darcsweb" [LogPID] Daemon $ do
+          let logf = logSyslog
+          logf $ "Starting on " ++ bind ++ ":" ++ show port
+          logf $ "Serving repositories from: " ++ absRepoDir
+          let cfg = mkConfig port bind absRepoDir title absStaticDir logf
+          runServer cfg
+      else do
+        let logf = logStdout
+        logf $ "Starting on " ++ bind ++ ":" ++ show port
+        logf $ "Serving repositories from: " ++ absRepoDir
+        let cfg = mkConfig port bind absRepoDir title absStaticDir logf
+        runServer cfg
+
+mkConfig :: Int -> String -> FilePath -> T.Text -> FilePath -> LogFunc
+         -> DarcsWebConfig
+mkConfig port bind repoDir title staticDir logf = DarcsWebConfig
+    { cfgPort      = port
+    , cfgBind      = bind
+    , cfgRepoDir   = repoDir
+    , cfgTitle     = title
+    , cfgStaticDir = staticDir
+    , cfgLog       = logf
+    }
+
+runServer :: DarcsWebConfig -> IO ()
+runServer cfg = do
+    let warpSettings = setPort (cfgPort cfg)
+                     $ setHost (fromString (cfgBind cfg))
+                       defaultSettings
+        scottyConfig = defaultOptions { verbose = 0, settings = warpSettings }
+    scottyOpts scottyConfig (app cfg)
+
+-- | Log to stdout (foreground mode)
+logStdout :: String -> IO ()
+logStdout msg = putStrLn ("[darcsweb] " ++ msg)
+
+-- | Log to syslog (daemon mode). Must be called inside withSyslog.
+logSyslog :: String -> IO ()
+logSyslog msg = withCStringLen msg $ \cstr ->
+    syslog (Just Daemon) Info cstr
+
+-- | Double-fork daemonize
+daemonize :: IO () -> IO ()
+daemonize action = do
+    _ <- forkProcess $ do
+      _ <- createSession
+      _ <- forkProcess $ do
+        redirectToDevNull
+        action
+      exitSuccess
+    exitSuccess
+
+redirectToDevNull :: IO ()
+redirectToDevNull = do
+    nullFd <- openDevNull
+    _ <- dupTo nullFd stdInput
+    _ <- dupTo nullFd stdOutput
+    _ <- dupTo nullFd stdError
+    return ()
+
+-- Open /dev/null using Posix.openFd. Works across unix package versions
+-- by using the FFI directly.
+foreign import ccall "open" c_open :: CString -> CInt -> IO CInt
+
+openDevNull :: IO Fd
+openDevNull = withCString "/dev/null" $ \cstr -> do
+    fd <- c_open cstr 2 -- O_RDWR = 2
+    return (Fd fd)
+
+-- | Map file extension to MIME type for static assets
+mimeType :: String -> TL.Text
+mimeType ".css"  = "text/css; charset=utf-8"
+mimeType ".js"   = "application/javascript"
+mimeType ".png"  = "image/png"
+mimeType ".jpg"  = "image/jpeg"
+mimeType ".jpeg" = "image/jpeg"
+mimeType ".gif"  = "image/gif"
+mimeType ".svg"  = "image/svg+xml"
+mimeType ".ico"  = "image/x-icon"
+mimeType ".woff" = "font/woff"
+mimeType ".woff2" = "font/woff2"
+mimeType _       = "application/octet-stream"
+
+-- | Build CSP header using formally verified builder from Rocq.
+--   The builder guarantees no semicolon injection within directive values.
+cspHeader :: BC.ByteString
+cspHeader = BC.pack $ CspPure.build_csp
+    [ ("default-src", "'none'")
+    , ("style-src",   "'self'")
+    , ("img-src",     "'self'")
+    , ("frame-ancestors", "'none'")
+    , ("base-uri",    "'none'")
+    , ("form-action", "'none'")
+    ]
+
+-- | WAI middleware that adds security response headers to every response.
+securityHeaders :: Middleware
+securityHeaders = modifyResponse $ mapResponseHeaders (++ secHeaders)
+  where
+    secHeaders =
+      [ ("X-Content-Type-Options", "nosniff")
+      , ("X-Frame-Options", "DENY")
+      , ("Referrer-Policy", "strict-origin-when-cross-origin")
+      , ("Permissions-Policy", "camera=(), microphone=(), geolocation=()")
+      , ("Content-Security-Policy", cspHeader)
+      , ("X-Robots-Tag", "noindex, nofollow")
+      ]
+
+app :: DarcsWebConfig -> ScottyM ()
+app cfg = do
+    middleware securityHeaders
+
+    -- Serve static files strictly from the configured static directory.
+    -- The route only matches /static/*, so no other paths are served.
+    -- The resolved file path is canonicalized and verified to be inside
+    -- the static directory before serving.
+    get (regex "^/static/.*") $ serveStatic cfg
+
+    -- Index page: list all repositories
+    get "/" $ do
+        now <- liftIO getCurrentTime
+        repos <- liftIO $ listRepos (cfgRepoDir cfg)
+        html $ TL.fromStrict $ renderRepoList now (cfgTitle cfg) repos
+
+    -- Repository summary
+    get "/repo/:name/summary" $ do
+        name <- pathParam "name"
+        withRepo cfg name $ \repoPath -> do
+            now <- liftIO getCurrentTime
+            repos <- liftIO $ listRepos (cfgRepoDir cfg)
+            let mRepoInfo = findRepo name repos
+            case mRepoInfo of
+              Nothing -> do
+                status status404
+                html $ TL.fromStrict $ render404 "Repository not found."
+              Just ri -> do
+                patches <- liftIO $ getRepoPatches repoPath
+                tags <- liftIO $ getRepoTags repoPath
+                html $ TL.fromStrict $ renderRepoSummary now name ri (take 10 patches) tags
+
+    -- Shortlog
+    get "/repo/:name/shortlog" $ do
+        name <- pathParam "name"
+        withRepo cfg name $ \repoPath -> do
+            now <- liftIO getCurrentTime
+            patches <- liftIO $ getRepoPatches repoPath
+            html $ TL.fromStrict $ renderShortLog now name patches
+
+    -- Full log
+    get "/repo/:name/log" $ do
+        name <- pathParam "name"
+        withRepo cfg name $ \repoPath -> do
+            now <- liftIO getCurrentTime
+            patches <- liftIO $ getRepoPatches repoPath
+            html $ TL.fromStrict $ renderFullLog now name patches
+
+    -- Tags
+    get "/repo/:name/tags" $ do
+        name <- pathParam "name"
+        withRepo cfg name $ \repoPath -> do
+            now <- liftIO getCurrentTime
+            tags <- liftIO $ getRepoTags repoPath
+            html $ TL.fromStrict $ renderTags now name tags
+
+    -- Tree view (root)
+    get "/repo/:name/tree" $ do
+        name <- pathParam "name"
+        withRepo cfg name $ \repoPath -> do
+            mEntries <- liftIO $ getRepoTree repoPath ""
+            case mEntries of
+              Nothing -> do
+                status status404
+                html $ TL.fromStrict $ render404 "Tree not found."
+              Just entries ->
+                html $ TL.fromStrict $ renderTree name "" entries
+
+    -- Tree view (subdirectory)
+    get (regex "^/repo/([^/]+)/tree/(.+)$") $ do
+        name <- pathParam "1"
+        subPath <- pathParam "2"
+        withRepo cfg name $ \repoPath -> do
+            let sub = T.unpack subPath
+            mEntries <- liftIO $ getRepoTree repoPath sub
+            case mEntries of
+              Nothing -> do
+                status status404
+                html $ TL.fromStrict $ render404 "Not found."
+              Just entries ->
+                html $ TL.fromStrict $ renderTree name subPath entries
+
+    -- Blob view (file contents)
+    get (regex "^/repo/([^/]+)/blob/(.+)$") $ do
+        name <- pathParam "1"
+        subPath <- pathParam "2"
+        withRepo cfg name $ \repoPath -> do
+            let sub = T.unpack subPath
+            mContent <- liftIO $ getRepoBlob repoPath sub
+            case mContent of
+              Nothing -> do
+                status status404
+                html $ TL.fromStrict $ render404 "Not found."
+              Just content ->
+                html $ TL.fromStrict $ renderBlob name subPath content
+
+    -- Single patch detail (diff view)
+    get "/repo/:name/patch/:hash" $ do
+        name <- pathParam "name"
+        patchHash <- pathParam "hash"
+        withRepo cfg name $ \repoPath -> do
+            mPatch <- liftIO $ getRepoPatch repoPath patchHash
+            case mPatch of
+              Nothing -> do
+                status status404
+                html $ TL.fromStrict $ render404 "Patch not found."
+              Just ps -> do
+                now <- liftIO getCurrentTime
+                html $ TL.fromStrict $ renderPatchDetail now name ps
+
+    -- 404 fallback
+    notFound $ do
+        status status404
+        html $ TL.fromStrict $ render404 "Page not found."
+
+-- | Serve a static file, strictly jailed to cfgStaticDir.
+--   Rejects any request whose canonicalized path escapes the static directory.
+serveStatic :: DarcsWebConfig -> ActionM ()
+serveStatic cfg = do
+    req <- request
+    -- Reconstruct the sub-path from the WAI pathInfo segments after "static"
+    let segments = pathInfo req
+        -- Drop the leading "static" segment
+        subSegments = drop 1 segments
+    -- Reject empty path, segments with "..", and any segment starting with "."
+    if null subSegments
+       || any (\s -> s == ".." || s == "." || T.null s) subSegments
+       || any (T.isPrefixOf ".") subSegments
+      then do
+        status status404
+        html $ TL.fromStrict $ render404 "Not found."
+      else do
+        let relPath = T.unpack (T.intercalate "/" subSegments)
+            candidate = cfgStaticDir cfg </> relPath
+        -- Canonicalize first, then check existence on the canonical path
+        -- to avoid TOCTOU race conditions with symlinks.
+        canonical <- liftIO $ canonicalizePath candidate
+        let jailDir = addTrailingSlash (cfgStaticDir cfg)
+        if not (jailDir `isPrefixOf` canonical)
+          then do
+            status status404
+            html $ TL.fromStrict $ render404 "Not found."
+          else do
+            exists <- liftIO $ doesFileExist canonical
+            if not exists
+              then do
+                status status404
+                html $ TL.fromStrict $ render404 "Not found."
+              else do
+                setHeader "Content-Type" (mimeType (takeExtension canonical))
+                setHeader "Cache-Control" "public, max-age=86400, immutable"
+                file canonical
+
+-- | Validate repo name and resolve path, then run an action.
+--   Rejects names with path separators or "..".
+--   Canonicalizes the resolved path and verifies it is inside the repos directory.
+withRepo :: DarcsWebConfig -> T.Text -> (FilePath -> ActionM ()) -> ActionM ()
+withRepo cfg name action
+    | T.any (== '/') name || T.any (== '\\') name || ".." `T.isInfixOf` name
+    || T.isPrefixOf "." name = do
+        status status404
+        html $ TL.fromStrict $ render404 "Invalid repository name."
+    | otherwise = do
+        let candidate = cfgRepoDir cfg </> T.unpack name
+        isRepo <- liftIO $ isDarcsRepo candidate
+        if not isRepo
+          then do
+            status status404
+            html $ TL.fromStrict $ render404 "Repository not found."
+          else do
+            -- Canonicalize to defeat symlink escapes
+            canonical <- liftIO $ canonicalizePath candidate
+            let jailDir = addTrailingSlash (cfgRepoDir cfg)
+            if jailDir `isPrefixOf` canonical
+              then action canonical
+              else do
+                status status403
+                html $ TL.fromStrict $ render404 "Access denied."
+
+-- | Ensure a directory path ends with exactly one /
+--   Uses formally verified implementation from Coq/Rocq.
+addTrailingSlash :: FilePath -> FilePath
+addTrailingSlash = PathPure.add_trailing_slash
+
+findRepo :: T.Text -> [RepoInfo] -> Maybe RepoInfo
+findRepo name = foldr (\r acc -> if riName r == name then Just r else acc) Nothing
+
hunk ./darcsweb.cabal 25
+                  , CspPure
hunk ./darcsweb.cabal 46
+                  , bytestring >= 0.10 && < 1
hunk ./darcsweb.cabal 61
+                  , Properties.Csp
addfile ./docker-compose.yml
hunk ./docker-compose.yml 1
+services:
+  darcsweb:
+    build: .
+    volumes:
+      - /srv/darcs:/srv/darcs:ro
+    expose:
+      - "3000"
+    restart: unless-stopped
+
+  nginx:
+    image: nginx:stable-alpine
+    ports:
+      - "80:80"
+      - "443:443"
+    volumes:
+      - ./nginx.conf:/etc/nginx/conf.d/default.conf:ro
+      - certbot_www:/var/www/certbot:ro
+      - certbot_conf:/etc/letsencrypt:ro
+    depends_on:
+      - darcsweb
+    restart: unless-stopped
+
+  certbot:
+    image: certbot/certbot
+    volumes:
+      - certbot_www:/var/www/certbot
+      - certbot_conf:/etc/letsencrypt
+    entrypoint: "/bin/sh -c 'trap exit TERM; while :; do certbot renew; sleep 12h & wait $${!}; done'"
+
+volumes:
+  certbot_www:
+  certbot_conf:
addfile ./nginx.conf
hunk ./nginx.conf 1
+# Rate limiting zone: 10 requests/second per IP, 10MB zone
+limit_req_zone $binary_remote_addr zone=darcsweb:10m rate=10r/s;
+
+server {
+    listen 80;
+    server_name darcs.example.com;
+    server_tokens off;
+
+    location /.well-known/acme-challenge/ {
+        root /var/www/certbot;
+    }
+
+    location / {
+        return 301 https://$host$request_uri;
+    }
+}
+
+server {
+    listen 443 ssl;
+    http2 on;
+    server_name darcs.example.com;
+    server_tokens off;
+
+    ssl_certificate     /etc/letsencrypt/live/darcs.example.com/fullchain.pem;
+    ssl_certificate_key /etc/letsencrypt/live/darcs.example.com/privkey.pem;
+
+    ssl_protocols TLSv1.2 TLSv1.3;
+    ssl_ciphers ECDHE-ECDSA-AES128-GCM-SHA256:ECDHE-RSA-AES128-GCM-SHA256:ECDHE-ECDSA-AES256-GCM-SHA384:ECDHE-RSA-AES256-GCM-SHA384;
+    ssl_prefer_server_ciphers off;
+
+    # OCSP stapling
+    ssl_stapling on;
+    ssl_stapling_verify on;
+
+    # Session resumption
+    ssl_session_timeout 1d;
+    ssl_session_cache shared:SSL:10m;
+    ssl_session_tickets off;
+
+    # HSTS: 2 years, include subdomains
+    add_header Strict-Transport-Security "max-age=63072000; includeSubDomains; preload" always;
+
+    # Limit request body and URI length
+    client_max_body_size 1k;
+    large_client_header_buffers 4 8k;
+
+    location / {
+        limit_req zone=darcsweb burst=20 nodelay;
+
+        proxy_pass http://darcsweb:3000;
+        proxy_set_header Host $host;
+        proxy_set_header X-Real-IP $remote_addr;
+        proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;
+        proxy_set_header X-Forwarded-Proto $scheme;
+
+        # Timeouts to prevent slow-loris attacks
+        proxy_connect_timeout 5s;
+        proxy_read_timeout 30s;
+        proxy_send_timeout 10s;
+    }
+}
hunk ./src/DarcsWeb/Darcs.hs 15
+  , maxPatchCount
hunk ./src/DarcsWeb/Darcs.hs 126
-          results = mapRL extractPatchListing patchRL
+          results = take maxPatchCount (mapRL extractPatchListing patchRL)
hunk ./src/DarcsWeb/Darcs.hs 150
--- | Get tags from a repository
+-- | Get tags from a repository.
+--   Scans the full patch set (not subject to maxPatchCount) since tags
+--   are rare and must all be visible regardless of repository size.
hunk ./src/DarcsWeb/Darcs.hs 155
-    allPatches <- getRepoPatches repoPath
-    return $ filter psIsTag allPatches
+    result <- try $ withRepositoryLocation YesUseCache repoPath $ RepoJob $ \repository -> do
+      patches <- readPatches repository
+      let patchRL = patchSet2RL patches
+          allInfos = mapRL extractPatchListing patchRL
+          tags = filter psIsTag allInfos
+      _ <- evaluate (length tags)
+      return tags
+    case result of
+      Left (_ :: SomeException) -> return []
+      Right val                 -> return val
+
+-- | Maximum number of patches to load per request (prevents DoS on large repos)
+maxPatchCount :: Int
+maxPatchCount = 500
addfile ./static/darcs-logo.png
binary ./static/darcs-logo.png
oldhex
*
newhex
*89504e470d0a1a0a0000000d49484452000000f20000004f0806000000d13c980f000000046741
*4d410000d6d8d44f583200000006624b474400ff00ff00ffa0bda7930000000970485973000000
*48000000480046c96b3e000027c14944415478daed9d79945cd57de73ff7bd577bab5749dd6ab5
*761990d40249d860096181218e890d1adba0c9022631038424834908e790e3648660e38913c764
*3c3e7646c6abc2d88c591d1b62b3884d366213621196415babd52da9b7eaeadade7ae78f5bafbb
*babad656230153df3ef75475d57befdebaef7eeffddddff68494923aeaa8e3bd0ded5437a08e3a
*ea3871d4895c471def03d4895c471def03d4895c471def03d4895c471def0318d51e689a268944
*e254b777462184a0a9a989402070aa9b52471d2784aa89fcd24b2ff195af7c85193657e94003d0
*0cb403b3800810041c2003a4800160084802d64c551e0a85b8fdf6db59b162c54cfea63aea38e9
*a89ac8a9548a83070f4e8bc84208344d430801d0029c019c2da53c07582ea59c27a56c04c28021
*a534004f086103269014421c17421c045e12423c0fec018e029ee779789e5773bbc2e130a6699e
*e42eafa38e9947d5446e6f6fe7631ffb584d44f6093c3232127afdf5d7cf344df393c0c7803384
*104d866188e6e6669a9a9a88442204020182c120baae0368b66d1b8ee3442ccb6a4ea7d35df178
*7c5d2291f894ebba1929e501e0295dd77fba6cd9b25f777676260cc3c075ddaadb170c06696e6e
*3ed5f7a08e3a4e18a25a624a296b22b1a669c4e3f1f0430f3d74fe134f3cf1277bf6ecb91898dd
*d0d020162d5ac4a2458b58b06001f3e7cfa7a3a38359b366110a85080402689ad2c1b9ae8b6ddb
*643219128904fdfdfdf4f6f6d2dbdbcb8103073872e408994c26397bf6ec9d1b376efcc1e5975f
*fef3d34f3f7db896b60a217c49a18e3adeb3a89ac8b52093c988eddbb7afb9efbefbfe72f7eedd
*971986d1d4d5d5c5ca952b39e79c7358b870214d4d4d44a3518410934857d89e7c920921f03c8f
*542ac5c8c808fbf6ed63e7ce9decddbb97a3478f9af3e6cddbb165cb96af7de2139f78b4a5a565
*c6f6d275d4f16ec78c12594ac98103075abefbddef5ef7e8a38ffe19b0b0bbbb9b0d1b36b066cd
*1ae6ce9d4b28141a27ef74ebf65751cff3c866b3f4f6f6b26bd72e9e79e6190e1c38105fbb76ed
*8fafbbeebaafae59b3665f4e4cafa38ef735668cc88ee3f0d4534fadfafad7bffec5dedede4b97
*2d5b665c74d145ac5fbf9ef6f6f6eac95bf87505a9379fd4870e1de2e9a79fe689279e90b66dbf
*7cf5d557ffede5975ffecb482452bb26ac8e3ade4398112267b359eebaebaedfbde79e7bfe594a
*b9ea231ff908975e7a298b172f46d3b4ea35ca9a44332422b7884a17a423905e757b584dd3701c
*87d75e7b8d071f7c903d7bf61cdfb871e397feeaaffeea7fcf9e3dbb2e6ad7f1bec50913399bcd
*6a5bb76ebd7cdbb66d5f9d3b77ee82cf7ce6336cdab489582c569349480b7b180d2ec290f8db62
*291591dd948e9ba9ce09cd5fa1878686f8f9cf7fce238f3c92fae0073ff84fb7de7aeb57dbdada
*52a7aca7eba8e31dc40911399bcdb275ebd63fdab66ddbd7162f5e3cf7b39ffd2c6bd7aead6d15
*06f48847a0c54168c5db223d813d62544d6650abb3699a6cdfbe9d7beeb9c73cf3cc33ffe5d65b
*6fbdbdadad2d7df2bab78e3a4e0ea64de41c892fddb66ddbbf2e5ebcb8f3da6baf65d5aa55789e
*579bad5983e06c1b3dec51ea2c01b8590d6b3080ac61b7eb4f284f3ffd343ff8c10fcc356bd6dc
*71ebadb7fe435b5b9b3d9ddfecba2e2fbcf002838383ef84c9aa0b580245bb41a09c5fde9ae94a
*eb78f7414ac9c2850b39f3cc33ab3e67da447ee8a187ceb9e38e3bee9e3f7ffef26baeb986b3ce
*3aabf42a2c29a9b4d20292e05c0b61946f877405e6b120d22e71a11275f84ab6279e78826ddbb6
*8d5d7ae9a59fbff1c61bbf371d6d76369be5939ffc248f3ffe38ef8036fc66e0ef81621e2d01e0
*bbc05fcc74a575bcfbe0ba2e9ffbdce7f8ce77be53f539557b76e563f7eedd1ddffce637ef6869
*69597ed5555771e699674ef1a892128426d1021274099ec0b305d21593f6c0020f29aa58668544
*e2e179dae4f3f55c1d5af13a3ccf4308c185175e88699ab3eebffffebf5bb66cd99b975d76d973
*d3ede4fcd71944088895f93e3cd315d6f1ee45ad2ec7351339914804b66edd7a4b3c1effe85557
*5dc5dab56b711c678a38ad473d024d0e5ac843688a749ea5e18cea38297d42807424d2f314d9cb
*40ba02cff1f0bc89e38c9887d1e4a005737578aa0e3b6ee0a627efa7354de3820b2ee0e0c1834b
*bef7bdef7d71c9922557ae5ebdfad8c9bc3975d4f14ea1e678e4fbeebbef63cf3ffffce7366cd8
*a05d70c105b8ae8bebbaf8810b9ee7a1451d8273b268511b7417295cd05cb4b04d60b6891eb3c7
*8f752d89634a246ed9e26425ae25f3eab009cccea245f2ead05db4889dabdb99d426c771080402
*5c76d96584c3e18ffef0873fbcde34cdba6f661def0bd444e4fdfbf7cfbefffefb6f6e6f6f6fbe
*ecb2cb884422b8ae3beee8e17912340fa3c5441a2e5e913fa9bbe8cd26182e9e27715d8915d770
*1d59f4780f0fd7c91de3e6ead05d8c16ab741d868bd16282aeeaf0dbe7ba2eededed6cdebc59db
*bd7bf7b5bff8c52fd69dea1b50471d3381aa896cdb36dffffef73fd5d7d7b771e3c68dcc9b370f
*cbb2d4aaeaafcaae8b08db10b2f1704b16820e2264e3b92e9ee7628d41e6b886eb78c8bce3242e
*aee39139ae6125c1f3541d849cca75846c4458d5e1e615dbb659b97225cb972feffac94f7e72fd
*f0f0703dab401def79544de437df7c73ce534f3df5b9850b1706ce3befbcdc0aec4d2aaee72183
*3652941793a57091ba8b9b77ae35a291e9d7716c6ffc38d7f1c81cd5b146b44975603855d541c0
*9954873fe90483412ebae822fafbfb376fdfbefdec537d13eaa8e34451b5b26bc78e1dbf333636
*b6f6e31fff38adadadd8767153ace7e556c40af0a48be74d9e47dc118144273cdf0401d98120d6
*b060924546e6ceada20ed7d3f1bca9c7799ec7b265cb38fdf4d3e73ef2c823bf7fc92597ec8c46
*a333e174aea1b29b1825fa5602362acb893303f5954320578cdc6b0465a02be6cdeea2b2b1f86d
*7b27dc593594e6bd01a5a1f7fb238dca027322191ef4bcdfaa53da43dfcd153b574e1482c9fd1c
*ca9552be006eeef73a4cf4f58c043b5445e4c1c1c1d0638f3df699e6e6e6507777f7b8726b0a24
*d86908786ed9b55e0052b878de545bac1917186d126148ac1181e77a936f8b645cec2edb031e38
*6939f5fc1c745d67ddba75fce8473fbae4d5575ffd970f7ff8c307a7d987738075c087500e1d1d
*a8d445c54c492e300a1c03de007e09bccccc90ba0d580d7403cb80cedc674d280285ca9c2b812c
*2a95d271a007780e783cf77f21c2c06654b6976213c36f812772ffb7021f052e0456a0523ae56f
*67d2402ff012f01fc08b5426d95c6065eef72ec95db335d7e7b3284d643f75d4303098fb9d7b51
*d9660e507902d3508e3b67e5fa7971aeee16a011358997dbaa79a8096b0c18418d83b773bff945
*20ce34511591df78e38d337a7b7b37ac5bb78ef6f6f692ab3180370ac618049a4a8f4d09c880c0
*75a712592071a58b96534e79ae9c7a5b0c1bafc2d8b793066602a4577ce5f63c8fa54b97128d46
*973ef9e4939bce3df7dc83357a6b45813f00ae43dd547fc5ab05ff15f857e01f99feccdc08fc21
*f0c7c02ad4609e096dfc0d2832ff2df074c177b350ce2ba7539cc8db80edc07ae08bc079949f48
*ce023e01fc19f06fc0975179da0ad10a5c0dfc112a5d54f4047fab444da2c7805f0177e5da5d6c
*70b500d7e7fa79318ab433d1cfbe54f2ebdcefde3e9d8b5445e45ffdea571b6ddb6e5fba7429ba
*ae9777867021d5631059e81068744bfe5411914843c7cb6a13c748d0021e046ca42e9181006e5a
*9f740d2d2011510b8fd25e644e4a277d58c735cb1bd5a3d1280b162c305e7ffdf5df49a552ffd6
*d0d050ad974704b80de56915994ec7e73017f81bd40a979dc6f96dc03f009f450dac994400381f
*d88a22ce4b79df0926ee4ab13bec011f4611a396cc86b3811b5193d14da801ee631ef03f814f31
*4d47a622f045e32e600b7011f03f80af33592a88015f01fe6406ebce6f430cb81835317e0e78ac
*d68b5454768d8c8c0476eddaf59168342a3a3b3b711c679216b858b19292b1b7828ced0f901914
*58631233a18a9596b88e0b610b6376160f17d751c5130e81d91964c046ea0e813919a4ee8c7fef
*7a2e465b062216aeeb60a73d75dd31899552d74f1dd149fc368095a0623b85102c5ebc98fefefe
*b30f1f3e3caf867efbcf9c38897d045033fd7fa2b6555907fe1a35b8669ac4f9381de53e1aaae1
*9c2ed44a3c9df4a41a4ad2b928ef3303b815b89c9927523eda5012c8270a3eff3470d53b5c37c0
*02d43d9d55eb89151bd6d3d3d376f4e8d1eee6e6665a5a5a8a7a712173aece0210ea1fc7115819
*0d713480c84d17be4ba531cb25ba284b705e0a4216ce983efe79a0c9c10f3fd65b1d22010b3b61
*206d81117309b4d93896207d308c336a201d31b13ee4c21e2512a139e3de5ed2136ad928583ba4
*94747474e0384ed7debd7b97af58b1a2b78a3e6b01ae616648eca309a8de435ea11bb5125772fa
*96b9e23275a2d051c4a924225e007c0078bdcab67d84137bf841036a62fb396a755f839a3c4f86
*034f336a627d14b59f8e00bf4f65175989da63dbb936e7f7b560421956e97ead039603bb6a6974
*45221f3f7e7c7132999cb778f16242a150d1fdb1d025811687608b8316f690aec01a3254b45291
*20073b2d70ec00b356a63066db186d133f7792302c406bb409cdcafbde1524f747308f6a50e8a3
*2d41e8109c6b119a63a3053d3c53c31a0e600d04f00ada2284a0a1a1814020103b74e8d02ae0c9
*2afa6c0d6a4f570d7c02d914bfb106d31f9ce7a2c4cd52c8020f033b518a9d31a6123982da6b5e
*86da5f976acb1c9472a95a22e72b7c7c4dbdbf75d073f55622fa6ad40437026c422995aa8197ab
*2f7f9b2450524bb5912e6b510ac35751cacb729285045e00ee4545a70da12680fcbed6500bc0e2
*5c5fff5e99b6b4024b9969221f3a7468b1e7798db1580c29258e33590fa0053c62cb3284da6d44
*9ebfb4de2610b382a4f6459096983244dc2149302109b6d993f6c89ea5293f69a1e294b5e064ad
*b393d6c91c17786e813e42820848624b32843badf1b6e8b320d2065a4b80d4dea88a69ce5d4f08
*41201020168b8937df7cf3b46c364b385c3136e12c2a8b3ea328a5c573c0e1dccd7598f8251a6a
*e65f026c44ad780db5dc381401cb4d02bf40298692555cebff02f7a0c4e86230726dad1509e07e
*e067c02114c966a188f2c7949f10e7a206f508d5492b07515aefdd401f13fb6b899a58da737d76
*016ad52bb71d6945ad8aafa208d852e6d821d4be7e67957df24be0aba809a2d456aa667d4935a2
*f542cff3f4603038ee8ee94308082fcd109897c989c379e34a9704e7db78c226f99b289eade5b5
*5b20343529e8d8ea3c09e64080f4db61155401180d2eb1e51982b37db24b1c5762dbae12a9f3ae
*a7053c1a966508769978a220a6518031c726647a8ced89225dbffd2ad797aeeb2493c905aeeb06
*a96c82585ae1fb24700bf043aab38d7e1db5cffd0ab591f951d420f2c5122fefbd406961ab2131
*a801fb2b4a1319ca0fe652fdf037c0b7996a4e7a0a7806b80f5854e2fc5928ad7418b59295c35b
*a889e1d754d633b4a1f6a17f4de9f1ef2bc0c8b5a11c4fc22869e60da64a0230754bd3035c899a
*ccf3bfd39890526ab6715724b210a20354f4503e91a554440b74a4f04a85210a0876da44854df2
*b751dc94da8e0943129a6ba13767f0d30938633aa36f04715220727d6167c1ce04693adb24d0a4
*3ed31a5c82f392648e8490b9c9418f7a444ecb10ec342997decb989382888e336a4c0a73d4759d
*6c363b379bcd0662b1583922eb2831b31c9e01fe0fd53b386450a4bf1c656bad168fe40aa801d0
*895a3517a048771ef0f132e78fa106d52e942db5bf427d316ac363c0f7283d285fcbd55d8ac8fe
*fe3d42e549e427a889a81a0c01df4089b82bcb1ce7dfe704e527f706e06bc07f41d9a7934c26ae
*ff98a3026f08bcdcb50750b6e43750d2dbb47c0aca1239e786d92484c0711c6cdb9e20b20746d4
*4486b3e56b1660ccb398d598c61a0980077a834ba0c9c533646e099124fb6264e21ea26052b047
*c138226868b2c65b1c3ec3c49867e02495692ad8e2a0c75c9c4abbcd0010cd600f84c71570fe6f
*eaebeb8bf6f6f6062be4f5d2a83ca05f41ed916a4112b5ffac85c8fe2ffa286a865f8fda3387a8
*4e81e5efdffb505241a5952c5a63db9e444d52a560e5ea86a964174c288d429417836d94385d0b
*8e0277a0f6c1c556218d89896130777c6b99eb35a1fa7f3af0956447505b836f006fd67a91b244
*8ec7e3bcf5d65b412104a6694e223252e00a0b5754e1cd278006083664c7ff9dd47b12cca48b63
*3b4aeb3de93b81957171a535313475d05b2db4d689cb57650016e062e3380608891002cbb2b02c
*0b2965404a59298042a3b2f83bc0f470bcc6e36328d1f52f5003a956f80ab78528e78e11cae672
*a9c9349605f65571dc5dc00ea69249e4ae7100b5b72da7b8b05164ab052e4a6aaa06475152d6ca
*2a8faf150235592d4539c46c44adee2fd47291b244761c874c464daaa9540ad334d1344d91590a
*453ed7ae9ca6c703f358906c5f083c08b43884e79be87eba690144b2d88e41e178110244637ad2
*84e1991ad9be20d690e25db8d322d46e4d52b6156f87c04c29c9c227723a9d269bcdce540e2edf
*d5713aa835e5c81fa3f679b5d8774b2146eda2733958a889a1127651593bdb49790db747f5ba80
*e9c04379df6d4229cbde699c097c01e5ad5775a2c8b2446e6e6ee6b4d34eb30e1e3cc8e8e828a9
*548a70389c233278839258c225d09a53584d8144ba82e49e18893722ca8b0b403308cfd368dd30
*8a1e53e3d798efc25b1ad6889197ca47106eb7303ac77072e3dc3335467636923e181e9fc7b5b7
*7466adf098d59dca4d2ac5dbe2a40dd28312c756abbb1082442241269341d33427f7f4c772f0c5
*d152f0bd74a6835a928075a06cd99548ec9b624aed7e7ccfa613318395ab7b265029c0a19aedce
*89e215e05a9437df0666d687a018ce4799dfaad5849727722010201a8d2600c6c6c6482412e8ba
*3e2e5edba310df6bd0724ebae86a285d41e2d506465f09215d3ff044c1e91184974174a95a69b5
*268bc6f50e89d762b96c9982d01c9b596bc720668f9f698e0449ecd7904edebd75c07a3984edd8
*34ad491697102424de0e9219f1f053716a9ac6e0e020994c86a54b97a6bababa2aed133c9492a8
*1caab57716626e0dc77603a75568e77328dbe6db28254c31328772f56e46395cbc1b63b34dca2b
*9b02d4d677fe3957a1146da5f6c84fa382467c3c0b5cc184b97075aede08133c1214b7910bd4f6
*4063221aad9c94d182bac73343640029e531804c26c3c0c0000d0d0d79fb641879ddc0d5823476
*a7d0a31e4248b56c657412bb63245e0d2ad215e8ec44d0c30b67707ce5ae00bddda4b92d899bd2
*919e5009eb031e4e9ea1d90b79b89a8963e988826b0ebd14c4b24234af4da2475cff633c4b23b9
*374a7c5710cfb427d9918f1d3b86e33884c3e1c14824526945f6a8acc85a8dda47d722ee35a31c
*4daac552caaf426fa24c5abfadf27adb5183fafc1ada70b290a5bc0520009c8db283578bc52857
*cc72b6f1bf6382c83ee9e2c0bfa33cce22a8fb9c1f2c538ec81194d4d58452505e4f697f0481f2
*3baf1a1589dcd8d8d8a3699ae7388ed6d7d7476767e7e4032c18d81962f42d8d50bb85d1e0225d
*41e64848a5aff526b8316ef995306b691a7dce188e54e2374265ddc4503fd557600994a9cbbf80
*68b2082e36c8bcdc304933e31f62be1824d91723ba388b16f270c60cb2fd41ccfe20d271264d28
*9665d1dfafac2e9aa6f550d986ec515929751e4aecfd2e95576fff86fd292a0cb25a547248e9c9
*956a91e40442e8de61645126a372f8435418e0cf28bfaf142889e92f296f9b964c28d0d6017fce
*54aef8c36f04e5e0518d7baf8f275113f7c515da5a352a12b9bbbbfb80aeeb092965737f7f3f89
*44a2a8f793d5076347fc18eb5c4b340b3de6a2853c95aad603cd9084bb4c1ad727b01c49e2a506
*d28742081d220bb3e32b3b28bfe9f4c13099c3213c4b106871685c99a6e1430358b649eab7513c
*0ff598191da42db0531ae6db82c4fe88f233c9791a0b6df2622b8460606080783c0ec08a152bde
*8a46abb2b0542248032a1ced53c0f3288fa611d4aa924191308cb2532e03ce4189513319f8d08d
*32873c4379bba4af85bf0c15adf46e4416d587e5301f15a5f53c8ad0875036da146a8c47508e20
*a7a126da6eca13c5caabb305b5ed282501b9b9bafe19e5d1570dfcb8f572c85473211f1589dcd9
*d979a8a1a1e168229168f61f36ded5d555f66912524268b64dd3da31a24bb268610fa440ba2a0c
*518f7a4824c71f6f21fe7c647cc58dff264a66c461cec57184261979b191c1a71bf0cc9ca42282
*24fb3dda7f6f98e64d19626b0ca43b99c8992321e22fce22db1f2c1a28918f9e9e1e2ccb42d3b4
*d4bc79f3dea8b2cf5e43ad60e5cc505194967313130a32dff3ca7774a8c6d65b0a95b4990b5071
*bdcfa1cc4009d4c0305113899e6b7f076a7077338d889b93040fe57956094dc0efe48adfd7be50
*a7513e734821fa9978aa475faeff4a11594779f25d88dad31e42e9242cd438f1933a0450d2d752
*94685dce7fdba6f2e435091589bc60c18281f6f6f6d7474747cf705d979e9e1e5a5b5b2729bd26
*410aa24b32ccf9e410a1b905ab60eed505b2fd41865e3170acbc6c275230fcba41c3876cf488c7
*e02e83ec58be6d5930f2864e6cad4774a189d6c694ebc7668f11e81ae5e8cfda48bd1d996a9746
*adc6c96492bebe3ea49444a3d123ab57afaef6712cbb51ce1bd5ae60bebd7626710045e6722244
*272afc6efcce14dc864254fafe54e22914b9aa0d35f527cae9f6fb7694ef3628096c7785bac328
*25d84626479ab94c4cd8b54cde3da805a36a540c356b6969b1d7ad5bf78c4fda818101fafbfb31
*4d736ac99ab8a114cd17f5a3cd4d6091295a6c328cf579a4871d4c333b71be95253d6a9319b331
*2d934cc22ea8234b3a6193ecf7b04b5cdb2283684bd07c613f6e388599358bb6f5d0a143a45229
*a494747575bdbc70e1c24a2e8a3e865076c5997cb2a38bd29226aa3c7e37b53f072a3f194021b2
*a8c17b2279b3de49bc0adccdcc99b4ca611fcabbcadf92a480ef50fdbdf127ee008ae07efa9f6a
*25020ff831b0bf9646571533ba7efdfa672291c871504e223d3d3da4d3e971af28bf98a6456051
*1ca36b149b2c4e896293253dec90cd4e3ddf9159dc401a3794c60da6314d73f231198b4cc2ae78
*7d7dfe28c145714c73721db66d333434445f9ff20e9452ba679f7df6636d6d6db5f8b8fe189549
*a2da9b5b094fa202f1ab7500e807fe17959569d540a22294b652bb53cac9828b4a87f47dded9c9
*e62d546692970b3e7f08a5f7a8760f3c5d58c08fa8ce657612aa123d56ad5af5665757d7736fbf
*fdf6659aa6118fc7e9ededa5a363f27e5d7aa0cd49e0e895c7633613c3cc9ae33ecf7e7282591b
*e2687313788624d23d48fcedd9e04d84414a0fb2a6895d4917a04bc4ec04a6199ca8031524d1d3
*d38369aaf1d0d4d47470d3a64d4fd6d8e126f04f2847f73f053e883221d5e2d4e1a272453d8c9a
*1434d46cec30f52606984ab26db9e36e46ed736b15237dcdec3da849643513b1d385300aeaf773
*5df97bff7cf87ed233921d320f03c0e75192c395a850c8566adbfb16eb0313a5717e0cf816c5f7
*e3362a30622fca8df283a85c6927a2e7f0ebb75052deeba8e08f9f308d09a3aa9bdfd6d696bdf8
*e28befddb76fdfc7851041cff3e8efef27180c128b4de800a487f2c9ae403201989612a9851fdd
*28a0f99c04adbf7b1cc7508be3ac0d16a30725c3bf6e1a575c4917cc4cb575981375e4303838c8
*f0f030a052019d71c6198f7477775725c6689ac6073ef001868686300cc3021e440d80d351a16c
*cb517b533faba2efe9a5a3564fffa6f5a26cbd2fa256010ba57cba96e2de5a1a6a5f9c0f0b65e2
*7a1cb5373b0b157ad78a227e43eed58fbe8189889be3a841b90335702dd49eec2a8a4f4682893d
*23b96bdc8452901523ac43f536ec5a904429f11ec8f5f5194c640c6dcdf5b96f5289e5fa32cd84
*dbacccdd872c135934f7e44a2fe535fc36ea7e3f8e5254ad40d9defd2c9a5126121f6ab9bed172
*6df6274733f77f02a510eb4389f2fb726d4981927a172d5a442da87a16dfb061c37ffcf8c73f7e
*299148acf7830d8e1c394267672781404029be3c41fc6d68b1b268c1325a6d4730d6ef62664df5
*1445016de78dd2fe07c7908deec4921083399767c924e6117f6996525c7982c4618fd976161128
*53872588ef93e375082148a5521c3b766c3c956f30183c7ec92597dc5d6d4eeb4020c09d77de59
*985c21894a4ce727a7cbcffe01132b86bf7a158b59f5aff3704d774fe150aedc9d576fbe96b670
*d57428beea1f077e5a659d262a1efa542185d213e4473df939adfd69db7f5ff8fbfdffa79b8278
*0c65e67abea06ebfcf41f57b61fffbb1422ec5fb7f1282c1daac91551379c58a1503e79f7ffe0f
*7efad39f7ec8300c03209d4e73f4e8d13c2d360cbeaad1b447d0bc26852c22750824c98311865e
*d5b0ac2c48683c33c9dcdf3f826cb4b10bcf6991ccd962317a70019923211030f49a46cb6fa171
*55ba641da3bf696070b78663651142397f0c0c0c60db3642085cd765f5ead5ffbe69d3a697a812
*428849124809f8a96d6622017aadf049faff234ee56f3fe57d5e758234c330b8fcf2cbefefe8e8
*d8e13f731820994c323434442693c1b24c52830efbb735113f080e696cd2d8394db5439ae480cb
*81bb1b19ebf3b0726278cbc7fa102d096cb2e3c74e942cc682380d1f3e866999589649f2b8cbfe
*bb9b48f479b93a3293ea18ed91ecff6113a901571d9f4c32303080652909534a896118bd9b376f
*dedad2d2722a0857471d330afdb6db6eabfae0f6f6f6743a9d1e7cf1c5173f01847d32fb490784
*1078d223734c23fe46081970d06216ae74b04661e8c508fbef9ac3f04b115c4f3ddbc9989da163
*4b3f5a83898b8b8733a5486c6c5332f064038ea5d2e2a6fb3446f784206421a216aee760c60583
*cfc538b0750ea36f06713d17d334492412e3490373e97dbcf3cf3fffce6baeb9e647a1d04c4401
*d651c7a945cd06f3cd9b37ff72c78e1d77efdebdfbcf0cc34008819412d334715d97502884a669
*986f6a8cbe3d87e09c66028d0e4e4ac73c1ec0333584965b195d0886d3c8680abb8ce54320a141
*c711596c73225862e8559d91dfb4139a6361cc7271923ae6f1209e2540a8f698a639be27f67374
*757474ecb8e69a6bbeddd8d838d39ad53aea3825a899c8edededd60d37dcf08fb7df7efbdaa347
*8faed7346d9ccc8ee38ce7c01242800dd98302a49173472890623d8199b5b05d132815d30c2031
*b301b2690bd72ad80dd8904de6d7a12609ffc98b52caf1f64929894422fd575e79e5df777777f7
*51471def13544de49e9e1e76ecd8e193e3506b6bebadfdfdfd3f0416f964014520df0bac52d60d
*2921794490ec83c616aba8e20ad48a3cfc4a10339173a1ad60b9f3499bdf861c99d3f178fc8e07
*1f7cf009d33489c562747777b364c912aa0c98a8a38e772544b9e0877c3cfae8a3dc74d34d8c8e
*8e323838483018a4b1b1f18af6f6f66f0821e6e693b9da6baa83051d9b07597ef3618c86e21e78
*a3afc4f8cd7f5f4ce670b8a8ef74c91f975b8973edb2878787bf76f8f0e1db1cc7c9068341110e
*8765474707b7dd761bebd7af67c18205e87a2d3e1d75d4f1ee4045222793491e7ef861fafafaf8
*c217be40369b15797b4e316fdebc6b3a3a3abe228468c92773b590528536cebe70848ecd432a8e
*38f7b40a7bc860e4f946faee9b4da627ace2956b70a4c927713c1edf7ae8d0a12f388e93a0e039
*c1b1588c356bd6c8db6ebb8dc6c646ce39e79c537d5feaa8a3265424f2bdf7decbf5d75f4f2693
*11b9447c9398248430e6cd9b77657b7bfb97354d6baf9dcc122955827a3dea129ced60c45c3c5b
*600f1bd871433dbb69fa24ce0c0f0f7ff3f0e1c35f761c6794c9241e7f350c835028c4860d1be4
*17bff845ce3df7dc53795feaa8a3269425f2debd7bb9faeaabd9b97367e12334455e4108a1b5b7
*b76f6e6f6fffb26118cba6d310994fadfc803a01424c8fc452ca91a1a1a13b8f1c39f20dc771d2
*4c90b858f16be7924b2e91dffef6b7993f7ffe49bb1175d471222849e4679f7d961b6fbc915dbb
*76153e0bb7b0f88ee3b2a9a9e983f3e7cfff6f9148e442409f8ea87d22c8afcfb6eddf1c3d7af4
*8ec1c1c19f799ee77bdef8a4f5284d68a9691ae79d779efcd6b7bec5aa55ab4e5afbeba863ba28
*ead9954ea779e185177c12fb2824af5e5082a3a3a3bbf7eddbf7e7434343ffe2baeef16929bf4e
*00be663a9148fc64fffefdd71e3f7efc61cff334544ca8ef879cdfe6fc60eff1e2791e3b77ee14
*afbcf2ca7894541d75bc9b5174457ee08107b8faeaab191b1b2bb502972b08218ca6a6a60fb5b7
*b7ff692c16db24843819b61d279bcdbe7afcf8f1bb8687877fe9ba6e8a0951dacb7bcd4f0353f8
*79feb1cc9d3b573ef0c0036cd8b0e114dc9a3aeaa81e45edc86d6d6dc53e2e4662bde055033429
*a588c7e32f2793c99b9b9b9b3fd2d6d67645341afd90a6698d33fd03a494a6699a7b8687871f1a
*1e1efe0fd3348f329147b81481f3b70afe3122ef1540eaba4e7373f349bd2175d4311d4c21722a
*95e2b5d75e23100814ee8dfdd7c295b998a8aa019ae338f6e0e0e063232323cfcd9a35ebcce6e6
*e68b1a1a1a3e1c0c06170a21c2d4a2c1ca8394d2761ce7583a9dde158fc71f4f24122f589635c8
*0481cbadc214d42b73edcd27b3ea1cc310bb76ed92cb972faf39acac8e3a4e26a688d6bdbdbd6c
*dcb89143870e1513a9f357e052a5a8b88d2288110a856647a3d1d363b1d859d168f4f4402030df
*308c165dd7fd407021d4e65a4ad538dbf3bcb4e338a38ee31ccd64326fa752a9d752a9d49e6c36
*db2fa5340bea2845629fc8f9253fcb457ea6cb71c5d7ba75ebe4f6eddb696c9c7161a28e3a660c
*d5ba688a129f55bb6f1e3fd634cd61d3347f353232f26b4dd3c2baae370483c1165dd75b8510b1
*402010360c23e8799e6b5956464a99715d77c4b2ac61d77593aeeb6698fc40ef20654c49799005
*6da6e07d1d75bc67514bd044b503be18398ada9f3dcfb33dcf1bb16d7b84c98fe12c3771e4e749
*ca276ee1b1b2c4f9a5eaa813ba8ef72caa257231c2c822dffbe22c4cec3bfdcf44de6bb9fd7739
*e43b6317aebe954a31db71a9df53471def294c21b26118747575d1dbdb8beb4e89112e468e4262
*163bbe98198b22af509accb2c8fb7264f628be472ee50c32a52ec330983f7f3e9a567522953aea
*3825286a477ef4d147d9b2658bc83d17a9d83eb850e935c504c5e40cfba5f6a5c55e8bf963166a
*948bbdfaeff3895aa8f4728bbce62bb92629bb162c58201f78e001ce3efbec537d9feaa8a32c8a
*8ad62323238c8e8e1612aa98f8ec7fae3361c62946e0135d8df3eb2a7c5f49bc2e74f6c8276e31
*4df53806060648266b793a6a1d759c1a149519376edcc84d37dde4ff5b4e64cd37e3f8c5ce7bcd
*2f56ae9879ef0bff372b94c273cc12d7ccafd32e6857bef9a998479704643018e4f39fff3c0b17
*2e3cd5f7a88e3a2aa228913b3b3bb9e8a28b686868285c018bed37f3895c48da72259f9c8544ad
*f69c62c7d84c25b4cde4c9269fc8852406a0b9b9597efad39f66c99272cfc2aea38e77074a6a71
*2ebef862eeb8e30e3f8f73a1f85accc1c229528aadca8544ab86f4a556ddc2f7f9af76893615db
*174f529ab5b6b672e79d77b26eddba537d7feaa8a32a94343f854221aebbee3a92c9a4fcd297be
*2432994cad0e16e5f6c2c5fe9f2e4a9991caeda14bfdcfca952be52db7dcc215575c412e0f7f1d
*75bceb5176a486c3616eb8e106868686e4f3cf3fcfb3cf3e5be86891af10aba4bcaa45a9552b64
*0def8b797ec9b6b6362ebcf042b965cb16aeb8e28a196e5e1d75bcb3a83af9debdf7decb962d5b
*fcd8e272ab6b29afac8a6da9b2cdd5345856f86cfc7d2814e2965b6e9173e6cce1da6baf251289
*d4d88575d471ea315dd9319f14c55669fff362c797c24c12b99ae3652010e0e69b6fe6c61b6f64
*ce9c39d3ec8a3aea38f5f87f00495769eebff9020000001974455874536f667477617265004164
*6f626520496d616765526561647971c9653c0000000049454e44ae426082
hunk ./static/style.css 1
-/* DarcsWeb - gitweb-inspired darcs repository browser */
+/* DarcsWeb ��� Technical Manuscript Theme
+   A warm, precise aesthetic for browsing darcs repositories.
+   Supports light/dark mode via prefers-color-scheme. */
+
+/* === Design Tokens === */
+:root {
+  /* Typography */
+  --font-body: -apple-system, BlinkMacSystemFont, "Segoe UI", Helvetica, Arial, sans-serif, "Apple Color Emoji", "Segoe UI Emoji";
+  --font-mono: "SF Mono", "Cascadia Code", "Fira Code", "JetBrains Mono", Menlo, Consolas, "Liberation Mono", monospace;
+  --size-xs: 0.6875rem;
+  --size-sm: 0.75rem;
+  --size-base: 0.875rem;
+  --size-md: 1rem;
+  --size-lg: 1.25rem;
+  --size-xl: 1.5rem;
+  --line-height: 1.6;
+  --line-mono: 1.5;
+
+  /* Spacing */
+  --space-1: 0.25rem;
+  --space-2: 0.5rem;
+  --space-3: 0.75rem;
+  --space-4: 1rem;
+  --space-5: 1.5rem;
+  --space-6: 2rem;
+  --space-8: 3rem;
+
+  /* Radii */
+  --radius-sm: 4px;
+  --radius-md: 6px;
+  --radius-lg: 8px;
+
+  /* Light mode colors */
+  --bg-page: #faf9f7;
+  --bg-surface: #ffffff;
+  --bg-muted: #f3f1ed;
+  --bg-header: #2d2a26;
+  --bg-footer: #2d2a26;
+
+  --text-primary: #1a1a1a;
+  --text-secondary: #5c574f;
+  --text-muted: #8a847a;
+  --text-inverse: #f3f1ed;
+  --text-link: #0d6e6e;
+  --text-link-hover: #095252;
+
+  --border-default: #e4e0d8;
+  --border-strong: #ccc7bc;
+  --border-subtle: #edeae4;
+
+  --accent: #0d6e6e;
+  --accent-bg: #e8f5f4;
+  --accent-subtle: #f0faf9;
+
+  --tag-bg: #fef3c7;
+  --tag-text: #92400e;
+  --tag-border: #fcd34d;
+
+  --diff-add-bg: #dafbe1;
+  --diff-add-text: #1a7f37;
+  --diff-del-bg: #ffd7d5;
+  --diff-del-text: #cf222e;
+  --diff-hunk-bg: #eee8fb;
+  --diff-hunk-text: #7c3aed;
+
+  --nav-bg: transparent;
+  --nav-active-bg: var(--bg-surface);
+  --nav-active-border: var(--accent);
+  --nav-hover-bg: var(--bg-muted);
+
+  --table-hover: #f8f6f2;
+  --table-stripe: #fcfbf9;
+
+  --shadow-sm: 0 1px 2px rgba(0,0,0,0.05);
+  --shadow-md: 0 2px 8px rgba(0,0,0,0.08);
+}
+
+@media (prefers-color-scheme: dark) {
+  :root {
+    --bg-page: #16171a;
+    --bg-surface: #1e1f23;
+    --bg-muted: #26272c;
+    --bg-header: #111214;
+    --bg-footer: #111214;
+
+    --text-primary: #e4e2de;
+    --text-secondary: #a09b93;
+    --text-muted: #6e6960;
+    --text-inverse: #1a1a1a;
+    --text-link: #4ecdc4;
+    --text-link-hover: #7ee0d9;
+
+    --border-default: #33343a;
+    --border-strong: #44464d;
+    --border-subtle: #28292e;
+
+    --accent: #4ecdc4;
+    --accent-bg: #1a2f2e;
+    --accent-subtle: #162524;
+
+    --tag-bg: #3d2e0a;
+    --tag-text: #fbbf24;
+    --tag-border: #78600f;
+
+    --diff-add-bg: #132a1c;
+    --diff-add-text: #56d364;
+    --diff-del-bg: #3d1117;
+    --diff-del-text: #ff7b72;
+    --diff-hunk-bg: #211b39;
+    --diff-hunk-text: #b28bf5;
+
+    --nav-hover-bg: var(--bg-muted);
+    --nav-active-bg: var(--bg-page);
+
+    --table-hover: #22232a;
+    --table-stripe: #1a1b20;
+
+    --shadow-sm: 0 1px 2px rgba(0,0,0,0.2);
+    --shadow-md: 0 2px 8px rgba(0,0,0,0.3);
+  }
+}
hunk ./static/style.css 124
-* {
+*, *::before, *::after {
hunk ./static/style.css 130
+html {
+  -webkit-text-size-adjust: 100%;
+  -webkit-font-smoothing: antialiased;
+  -moz-osx-font-smoothing: grayscale;
+}
+
hunk ./static/style.css 137
-  font-family: sans-serif;
-  font-size: 13px;
-  color: #000;
-  background: #fff;
+  font-family: var(--font-body);
+  font-size: var(--size-base);
+  line-height: var(--line-height);
+  color: var(--text-primary);
+  background: var(--bg-page);
+  min-height: 100vh;
+  display: flex;
+  flex-direction: column;
hunk ./static/style.css 148
-  color: #0000cc;
+  color: var(--text-link);
hunk ./static/style.css 150
+  transition: color 0.15s ease;
hunk ./static/style.css 154
+  color: var(--text-link-hover);
hunk ./static/style.css 156
+  text-underline-offset: 2px;
hunk ./static/style.css 159
-pre {
-  font-family: monospace;
-  font-size: 12px;
+pre, code {
+  font-family: var(--font-mono);
+  font-size: var(--size-sm);
+  line-height: var(--line-mono);
hunk ./static/style.css 166
-  font-size: 18px;
-  font-weight: bold;
-  margin-bottom: 8px;
+  font-size: var(--size-xl);
+  font-weight: 700;
+  letter-spacing: -0.02em;
+  margin-bottom: var(--space-4);
+  color: var(--text-primary);
hunk ./static/style.css 174
-  font-size: 14px;
-  font-weight: bold;
-  margin: 16px 0 8px 0;
-  padding-bottom: 4px;
-  border-bottom: 1px solid #d9d8d1;
+  font-size: var(--size-md);
+  font-weight: 600;
+  letter-spacing: -0.01em;
+  margin: var(--space-6) 0 var(--space-3) 0;
+  padding-bottom: var(--space-2);
+  border-bottom: 2px solid var(--border-default);
+  color: var(--text-primary);
hunk ./static/style.css 185
-  background: #d9d8d1;
-  padding: 8px 12px;
-  font-size: 18px;
-  font-weight: bold;
-  border-bottom: 1px solid #808080;
+  background: var(--bg-header);
+  padding: var(--space-3) var(--space-5);
+  font-size: var(--size-base);
+  display: flex;
+  align-items: center;
+  gap: var(--space-2);
+  border-bottom: 3px solid var(--accent);
+  position: sticky;
+  top: 0;
+  z-index: 100;
hunk ./static/style.css 198
-  color: #000;
+  color: var(--text-inverse);
hunk ./static/style.css 202
+  font-weight: 500;
+  opacity: 0.75;
+  transition: opacity 0.15s ease;
hunk ./static/style.css 207
+.page-header a:hover {
+  opacity: 1;
+  text-decoration: none;
+}
+
hunk ./static/style.css 213
-  height: 28px;
+  height: 24px;
hunk ./static/style.css 216
+  filter: brightness(0) invert(1);
+  opacity: 0.9;
hunk ./static/style.css 220
-
-.page-header a:hover {
-  text-decoration: underline;
-}
-
hunk ./static/style.css 221
-  padding: 12px;
-  min-height: 400px;
+  flex: 1;
+  padding: var(--space-6) var(--space-5);
+  max-width: 1100px;
+  width: 100%;
+  margin: 0 auto;
hunk ./static/style.css 229
-  background: #d9d8d1;
-  padding: 6px 12px;
-  border-top: 1px solid #808080;
-  font-size: 11px;
-  color: #555;
+  background: var(--bg-footer);
+  padding: var(--space-3) var(--space-5);
+  font-size: var(--size-xs);
+  color: var(--text-muted);
hunk ./static/style.css 234
+  margin-top: auto;
+  border-top: 1px solid var(--border-subtle);
hunk ./static/style.css 239
-  color: #333;
+  color: var(--text-muted);
+  opacity: 0.8;
hunk ./static/style.css 243
+.page-footer a:hover {
+  color: var(--text-link);
+  opacity: 1;
+}
+
hunk ./static/style.css 250
-  margin: 8px 0 16px 0;
-  padding: 4px 0;
-  border-bottom: 1px solid #d9d8d1;
+  margin: var(--space-3) 0 var(--space-5) 0;
+  display: flex;
+  gap: var(--space-1);
+  border-bottom: 2px solid var(--border-default);
+  padding-bottom: 0;
+  overflow-x: auto;
+  -webkit-overflow-scrolling: touch;
hunk ./static/style.css 261
-  padding: 4px 12px;
-  margin-right: 2px;
-  color: #0000cc;
-  background: #edece6;
-  border: 1px solid #d9d8d1;
-  border-bottom: none;
-  font-size: 12px;
+  padding: var(--space-2) var(--space-4);
+  color: var(--text-secondary);
+  font-size: var(--size-sm);
+  font-weight: 500;
+  border-bottom: 2px solid transparent;
+  margin-bottom: -2px;
+  transition: color 0.15s ease, border-color 0.15s ease;
+  white-space: nowrap;
+  text-decoration: none;
hunk ./static/style.css 273
-  background: #d9d8d1;
+  color: var(--text-primary);
+  background: var(--nav-hover-bg);
+  border-radius: var(--radius-sm) var(--radius-sm) 0 0;
hunk ./static/style.css 280
-  background: #fff;
-  border-bottom: 1px solid #fff;
-  font-weight: bold;
-  color: #000;
+  color: var(--accent);
+  border-bottom-color: var(--accent);
+  font-weight: 600;
hunk ./static/style.css 289
+  border-spacing: 0;
hunk ./static/style.css 294
-  padding: 4px 8px;
-  background: #edece6;
-  border-bottom: 1px solid #d9d8d1;
-  font-size: 12px;
-  font-weight: bold;
-  color: #333;
+  padding: var(--space-2) var(--space-3);
+  background: var(--bg-muted);
+  border-bottom: 2px solid var(--border-default);
+  font-size: var(--size-xs);
+  font-weight: 600;
+  text-transform: uppercase;
+  letter-spacing: 0.05em;
+  color: var(--text-secondary);
hunk ./static/style.css 305
-  border-bottom: 1px solid #eee;
+  border-bottom: 1px solid var(--border-subtle);
+  transition: background 0.1s ease;
hunk ./static/style.css 310
-  background: #f6f5ee;
+  background: var(--table-hover);
hunk ./static/style.css 314
-  padding: 4px 8px;
+  padding: var(--space-2) var(--space-3);
hunk ./static/style.css 320
-  font-family: monospace;
+  font-family: var(--font-mono);
+  font-size: var(--size-sm);
+  color: var(--text-secondary);
hunk ./static/style.css 327
-  font-weight: bold;
+  font-weight: 600;
+  color: var(--text-link);
hunk ./static/style.css 333
-  font-size: 12px;
+  font-size: var(--size-sm);
hunk ./static/style.css 337
-  color: #555;
+  color: var(--text-muted);
+  padding: var(--space-1) var(--space-2);
+  border-radius: var(--radius-sm);
+  transition: color 0.15s ease, background 0.15s ease;
hunk ./static/style.css 344
-  color: #0000cc;
+  color: var(--text-link);
+  background: var(--accent-bg);
+  text-decoration: none;
hunk ./static/style.css 352
-  color: #666;
-  font-family: monospace;
-  font-size: 12px;
-  width: 150px;
+  color: var(--text-muted);
+  font-family: var(--font-mono);
+  font-size: var(--size-sm);
+  width: 140px;
hunk ./static/style.css 360
-  font-style: italic;
-  color: #006699;
+  color: var(--text-secondary);
+  font-weight: 500;
hunk ./static/style.css 369
-  color: #000;
+  color: var(--text-primary);
+  font-weight: 500;
hunk ./static/style.css 374
-  color: #0000cc;
+  color: var(--text-link);
hunk ./static/style.css 379
-  font-size: 12px;
+  font-size: var(--size-sm);
hunk ./static/style.css 384
-  color: #555;
+  color: var(--text-muted);
+  padding: var(--space-1) var(--space-2);
+  border-radius: var(--radius-sm);
hunk ./static/style.css 389
+.shortlog td.actions a:hover {
+  color: var(--text-link);
+  background: var(--accent-bg);
+  text-decoration: none;
+}
+
hunk ./static/style.css 396
-  background: #ffffee;
+  background: var(--tag-bg);
hunk ./static/style.css 399
+.shortlog tr.tag-row:hover {
+  background: var(--tag-bg);
+  filter: brightness(0.97);
+}
+
hunk ./static/style.css 407
-  background: #ffc800;
-  color: #000;
-  font-size: 10px;
-  font-weight: bold;
-  padding: 1px 4px;
-  border-radius: 3px;
-  margin-right: 4px;
+  background: var(--tag-bg);
+  color: var(--tag-text);
+  font-size: var(--size-xs);
+  font-weight: 700;
+  padding: 1px 6px;
+  border-radius: var(--radius-sm);
+  border: 1px solid var(--tag-border);
+  margin-right: var(--space-1);
hunk ./static/style.css 416
+  letter-spacing: 0.04em;
+  text-transform: uppercase;
hunk ./static/style.css 422
-  font-weight: bold;
-  color: #006600;
+  font-weight: 600;
+  color: var(--text-link);
hunk ./static/style.css 428
-  color: #666;
-  font-family: monospace;
-  font-size: 12px;
-  width: 150px;
+  color: var(--text-muted);
+  font-family: var(--font-mono);
+  font-size: var(--size-sm);
+  width: 140px;
hunk ./static/style.css 435
-  color: #006699;
-  font-style: italic;
+  color: var(--text-secondary);
+  font-weight: 500;
hunk ./static/style.css 441
-  margin-bottom: 16px;
-  padding: 8px;
-  border: 1px solid #d9d8d1;
-  background: #fafaf6;
+  margin-bottom: var(--space-4);
+  padding: var(--space-4);
+  border: 1px solid var(--border-default);
+  border-radius: var(--radius-md);
+  background: var(--bg-surface);
+  box-shadow: var(--shadow-sm);
+  transition: box-shadow 0.15s ease;
hunk ./static/style.css 450
+.log-entry:hover {
+  box-shadow: var(--shadow-md);
+}
+
hunk ./static/style.css 455
-  background: #ffffee;
-  border-color: #e0d000;
+  background: var(--tag-bg);
+  border-color: var(--tag-border);
hunk ./static/style.css 463
-  margin-bottom: 4px;
+  gap: var(--space-3);
+  margin-bottom: var(--space-2);
hunk ./static/style.css 468
-  font-weight: bold;
-  font-size: 14px;
+  font-weight: 600;
+  font-size: var(--size-base);
+  min-width: 0;
hunk ./static/style.css 474
-  color: #000;
+  color: var(--text-primary);
hunk ./static/style.css 478
-  color: #0000cc;
+  color: var(--text-link);
hunk ./static/style.css 482
-  color: #666;
-  font-family: monospace;
-  font-size: 12px;
+  color: var(--text-muted);
+  font-family: var(--font-mono);
+  font-size: var(--size-sm);
hunk ./static/style.css 486
+  flex-shrink: 0;
hunk ./static/style.css 490
-  font-size: 12px;
-  color: #006699;
-  margin-bottom: 4px;
+  font-size: var(--size-sm);
+  color: var(--text-secondary);
+  margin-bottom: var(--space-2);
hunk ./static/style.css 496
-  margin-top: 8px;
+  margin-top: var(--space-3);
hunk ./static/style.css 500
-  background: #fff;
-  padding: 6px 8px;
-  border: 1px solid #eee;
-  color: #333;
+  background: var(--bg-muted);
+  padding: var(--space-3) var(--space-4);
+  border-radius: var(--radius-sm);
+  color: var(--text-primary);
hunk ./static/style.css 506
+  font-size: var(--size-sm);
hunk ./static/style.css 510
-  margin-top: 6px;
+  margin-top: var(--space-2);
hunk ./static/style.css 514
-  color: #555;
-  font-size: 11px;
+  color: var(--text-secondary);
+  font-size: var(--size-xs);
hunk ./static/style.css 517
+  padding: var(--space-2) var(--space-3);
+  background: var(--bg-muted);
+  border-radius: var(--radius-sm);
hunk ./static/style.css 524
-  font-size: 18px;
-  margin-bottom: 12px;
-  padding-bottom: 8px;
-  border-bottom: 1px solid #d9d8d1;
+  font-size: var(--size-lg);
+  margin-bottom: var(--space-4);
+  padding-bottom: var(--space-3);
+  border-bottom: 2px solid var(--border-default);
hunk ./static/style.css 532
-  margin-bottom: 16px;
+  margin-bottom: var(--space-5);
+  background: var(--bg-surface);
+  border: 1px solid var(--border-default);
+  border-radius: var(--radius-md);
+  overflow: hidden;
hunk ./static/style.css 540
-  background: none;
+  background: var(--bg-muted);
hunk ./static/style.css 542
+  border-bottom: 1px solid var(--border-subtle);
hunk ./static/style.css 544
-  padding: 2px 12px 2px 0;
-  font-weight: bold;
-  color: #333;
+  padding: var(--space-2) var(--space-3);
+  font-weight: 600;
+  font-size: var(--size-sm);
+  color: var(--text-secondary);
hunk ./static/style.css 549
+  text-transform: none;
+  letter-spacing: normal;
hunk ./static/style.css 555
-  padding: 2px 0;
+  border-bottom: 1px solid var(--border-subtle);
+  padding: var(--space-2) var(--space-3);
+  font-size: var(--size-sm);
hunk ./static/style.css 560
+.patch-meta tr:last-child th,
+.patch-meta tr:last-child td {
+  border-bottom: none;
+}
+
hunk ./static/style.css 566
-  font-family: monospace;
-  font-size: 12px;
-  color: #666;
+  font-family: var(--font-mono);
+  font-size: var(--size-sm);
+  color: var(--text-muted);
+  word-break: break-all;
hunk ./static/style.css 573
-  background: #fafaf6;
-  padding: 8px;
-  border: 1px solid #d9d8d1;
+  background: var(--bg-muted);
+  padding: var(--space-3) var(--space-4);
+  border-radius: var(--radius-md);
hunk ./static/style.css 578
+  font-size: var(--size-sm);
hunk ./static/style.css 582
-  background: #f5f5f0;
-  padding: 8px;
-  border: 1px solid #d9d8d1;
-  color: #333;
+  background: var(--bg-muted);
+  padding: var(--space-3) var(--space-4);
+  border-radius: var(--radius-md);
+  color: var(--text-secondary);
hunk ./static/style.css 587
+  font-size: var(--size-sm);
hunk ./static/style.css 590
+/* === Diff Viewer === */
hunk ./static/style.css 592
-  background: #fafafa;
-  padding: 8px;
-  border: 1px solid #d9d8d1;
+  background: var(--bg-surface);
+  padding: 0;
+  border: 1px solid var(--border-default);
+  border-radius: var(--radius-md);
hunk ./static/style.css 598
+  font-size: var(--size-sm);
+  line-height: 1.55;
hunk ./static/style.css 603
-  color: #22863a;
-  background: #e6ffec;
+  display: block;
+  color: var(--diff-add-text);
+  background: var(--diff-add-bg);
+  padding: 0 var(--space-3);
hunk ./static/style.css 610
-  color: #cb2431;
-  background: #ffeef0;
+  display: block;
+  color: var(--diff-del-text);
+  background: var(--diff-del-bg);
+  padding: 0 var(--space-3);
hunk ./static/style.css 617
-  color: #6f42c1;
-  line-height: 1.4;
-  tab-size: 8;
+  display: block;
+  color: var(--diff-hunk-text);
+  background: var(--diff-hunk-bg);
+  padding: var(--space-1) var(--space-3);
+  font-weight: 600;
+  border-top: 1px solid var(--border-default);
+  border-bottom: 1px solid var(--border-default);
+  margin-top: var(--space-1);
hunk ./static/style.css 627
-/* === Description & Empty states === */
+.diff-hunk:first-child {
+  margin-top: 0;
+  border-top: none;
+  border-radius: var(--radius-md) var(--radius-md) 0 0;
+}
+
+/* === Description & Empty States === */
hunk ./static/style.css 635
-  color: #555;
+  color: var(--text-secondary);
hunk ./static/style.css 637
-  margin-bottom: 8px;
+  margin-bottom: var(--space-3);
+  padding: var(--space-3) var(--space-4);
+  background: var(--accent-subtle);
+  border-left: 3px solid var(--accent);
+  border-radius: 0 var(--radius-sm) var(--radius-sm) 0;
hunk ./static/style.css 645
-  color: #999;
+  color: var(--text-muted);
hunk ./static/style.css 647
-  padding: 20px 0;
+  padding: var(--space-8) 0;
+  text-align: center;
hunk ./static/style.css 652
-  margin-top: 4px;
+  margin-top: var(--space-2);
hunk ./static/style.css 656
-  color: #555;
+  color: var(--text-muted);
+  font-size: var(--size-sm);
hunk ./static/style.css 661
+.more a:hover {
+  color: var(--text-link);
+}
+
hunk ./static/style.css 667
-  margin: 8px 0 12px 0;
-  font-size: 13px;
+  margin: var(--space-3) 0 var(--space-4) 0;
+  font-size: var(--size-sm);
+  color: var(--text-secondary);
+  padding: var(--space-2) var(--space-3);
+  background: var(--bg-muted);
+  border-radius: var(--radius-sm);
+  overflow-x: auto;
+  white-space: nowrap;
hunk ./static/style.css 678
-  color: #0000cc;
+  color: var(--text-link);
+  font-weight: 500;
hunk ./static/style.css 683
-  width: 20px;
+  width: 28px;
hunk ./static/style.css 685
-  padding: 3px 4px;
+  padding: var(--space-2) var(--space-1);
+  font-size: var(--size-base);
hunk ./static/style.css 690
-  padding: 3px 8px;
+  padding: var(--space-2) var(--space-3);
hunk ./static/style.css 694
-  color: #000;
+  color: var(--text-primary);
+  font-weight: 500;
hunk ./static/style.css 699
-  color: #0000cc;
+  color: var(--text-link);
hunk ./static/style.css 704
-  color: #666;
-  font-family: monospace;
-  font-size: 12px;
-  width: 80px;
+  color: var(--text-muted);
+  font-family: var(--font-mono);
+  font-size: var(--size-sm);
+  width: 90px;
hunk ./static/style.css 713
-  margin-top: 12px;
+  margin-top: var(--space-4);
hunk ./static/style.css 717
-  background: #fafaf6;
-  padding: 8px;
-  border: 1px solid #d9d8d1;
+  background: var(--bg-surface);
+  padding: var(--space-4);
+  border: 1px solid var(--border-default);
+  border-radius: var(--radius-md);
hunk ./static/style.css 723
-  line-height: 1.4;
+  line-height: var(--line-mono);
hunk ./static/style.css 728
-  font-family: monospace;
-  font-size: 12px;
+  font-family: var(--font-mono);
+  font-size: var(--size-sm);
+}
+
+/* === Mobile Responsiveness === */
+@media (max-width: 768px) {
+  .page-header {
+    padding: var(--space-2) var(--space-3);
+  }
+
+  .page-body {
+    padding: var(--space-4) var(--space-3);
+  }
+
+  h1 {
+    font-size: var(--size-lg);
+  }
+
+  /* Scrollable tables on mobile */
+  table {
+    display: block;
+    overflow-x: auto;
+    -webkit-overflow-scrolling: touch;
+  }
+
+  thead, tbody, tr {
+    display: table;
+    width: 100%;
+    table-layout: fixed;
+  }
+
+  thead {
+    display: none;
+  }
+
+  /* Repo list: stack on mobile */
+  .repo-list tbody tr {
+    display: flex;
+    flex-wrap: wrap;
+    padding: var(--space-3);
+    gap: var(--space-1);
+    border-bottom: 1px solid var(--border-default);
+  }
+
+  .repo-list td {
+    padding: 0;
+    border: none;
+  }
+
+  .repo-list td.repo-name {
+    width: 100%;
+    font-size: var(--size-md);
+  }
+
+  .repo-list td.actions {
+    margin-left: auto;
+  }
+
+  /* Shortlog: compact on mobile */
+  .shortlog tbody tr {
+    display: flex;
+    flex-wrap: wrap;
+    padding: var(--space-2) var(--space-3);
+    gap: var(--space-1);
+  }
+
+  .shortlog td {
+    padding: 0;
+    border: none;
+  }
+
+  .shortlog td.date {
+    width: auto;
+    order: 2;
+  }
+
+  .shortlog td.author {
+    width: auto;
+    max-width: none;
+    order: 3;
+  }
+
+  .shortlog td.subject {
+    width: 100%;
+    order: 1;
+  }
+
+  .shortlog td.actions {
+    order: 4;
+    margin-left: auto;
+  }
+
+  /* Log entries: full width */
+  .log-header {
+    flex-direction: column;
+    gap: var(--space-1);
+  }
+
+  /* Patch meta: stack */
+  .patch-meta th,
+  .patch-meta td {
+    display: block;
+    width: 100%;
+    text-align: left;
+  }
+
+  .patch-meta th {
+    padding-bottom: 0;
+    border-bottom: none;
+  }
+
+  /* Repo nav: scroll */
+  .repo-nav {
+    gap: 0;
+  }
+
+  .repo-nav a {
+    padding: var(--space-2) var(--space-3);
+    font-size: var(--size-xs);
+  }
+}
+
+@media (max-width: 480px) {
+  .page-body {
+    padding: var(--space-3) var(--space-2);
+  }
+
+  .blob-content pre,
+  .patch-diff pre.diff {
+    border-radius: 0;
+    margin-left: calc(var(--space-2) * -1);
+    margin-right: calc(var(--space-2) * -1);
+    padding: var(--space-3);
+  }
+}
+
+/* === Print === */
+@media print {
+  .page-header,
+  .page-footer,
+  .repo-nav {
+    display: none;
+  }
+
+  .page-body {
+    padding: 0;
+    max-width: none;
+  }
+
+  body {
+    background: white;
+    color: black;
+  }
+
+  a {
+    color: black;
+    text-decoration: underline;
+  }
+
+  .diff-add { background: #e6ffe6; }
+  .diff-del { background: #ffe6e6; }
adddir ./test
adddir ./test/Properties
addfile ./test/Properties/Csp.hs
hunk ./test/Properties/Csp.hs 1
+{-# LANGUAGE OverloadedStrings #-}
+
+module Properties.Csp (tests) where
+
+import Test.QuickCheck
+import qualified CspPure
+
+-- --------------------------------------------------------------------------
+-- sanitize_value properties
+-- --------------------------------------------------------------------------
+
+prop_sanitize_no_semicolons :: String -> Bool
+prop_sanitize_no_semicolons s =
+    ';' `notElem` CspPure.sanitize_value s
+
+prop_sanitize_empty :: Bool
+prop_sanitize_empty = CspPure.sanitize_value "" == ""
+
+prop_sanitize_preserves_safe :: String -> Property
+prop_sanitize_preserves_safe s =
+    all (/= ';') s ==>
+    CspPure.sanitize_value s == s
+
+-- --------------------------------------------------------------------------
+-- build_directive properties
+-- --------------------------------------------------------------------------
+
+prop_directive_starts_with_name :: String -> String -> Property
+prop_directive_starts_with_name name value =
+    not (null name) ==>
+    let result = CspPure.build_directive name value
+    in take (length name) result == name
+
+prop_directive_has_space :: String -> String -> Property
+prop_directive_has_space name value =
+    not (null name) ==>
+    let result = CspPure.build_directive name value
+    in result !! length name == ' '
+
+-- --------------------------------------------------------------------------
+-- build_csp properties
+-- --------------------------------------------------------------------------
+
+prop_csp_empty :: Bool
+prop_csp_empty = CspPure.build_csp [] == ""
+
+prop_csp_single :: Bool
+prop_csp_single =
+    CspPure.build_csp [("default-src", "'none'")] ==
+    "default-src 'none'"
+
+-- | Directive names are programmer-controlled (no semicolons).
+--   Values are arbitrary (may contain semicolons from user input).
+--   The builder must ensure no semicolons leak into values.
+prop_csp_no_value_semicolons :: Property
+prop_csp_no_value_semicolons =
+    forAll genDirectives $ \directives ->
+    let result = CspPure.build_csp directives
+        parts = splitOnSemiSpace result
+    in all (notElem ';') parts
+  where
+    genDirectives = do
+      n <- choose (1, 5)
+      vectorOf n genDirective
+    genDirective = do
+      name <- elements ["default-src", "style-src", "img-src", "script-src",
+                         "frame-ancestors", "base-uri", "form-action"]
+      value <- arbitrary
+      return (name, value)
+    splitOnSemiSpace [] = [""]
+    splitOnSemiSpace (';':' ':rest) = "" : splitOnSemiSpace rest
+    splitOnSemiSpace (c:rest) = case splitOnSemiSpace rest of
+      (h:t) -> (c:h):t
+      []    -> [[c]]
+
+-- --------------------------------------------------------------------------
+-- Test runner
+-- --------------------------------------------------------------------------
+
+tests :: IO Bool
+tests = fmap and $ sequence
+    [ run "sanitize: no semicolons"        (property prop_sanitize_no_semicolons)
+    , run "sanitize: empty"                (property prop_sanitize_empty)
+    , run "sanitize: preserves safe"       prop_sanitize_preserves_safe
+    , run "directive: starts with name"    prop_directive_starts_with_name
+    , run "directive: has space separator"  prop_directive_has_space
+    , run "csp: empty list"                (property prop_csp_empty)
+    , run "csp: single directive"          (property prop_csp_single)
+    , run "csp: no value semicolons"       prop_csp_no_value_semicolons
+    ]
+  where
+    run name prop = do
+      putStr $ "  " ++ name ++ ": "
+      r <- quickCheckWithResult stdArgs { maxSuccess = 200 } prop
+      return (isSuccess r)
addfile ./test/Properties/Html.hs
hunk ./test/Properties/Html.hs 1
+{-# LANGUAGE OverloadedStrings #-}
+
+module Properties.Html (tests) where
+
+import Test.QuickCheck
+import qualified Data.Text as T
+
+import DarcsWeb.Html (esc, highlightDiff, shortAuthor, formatSize, formatAbsolute)
+
+-- --------------------------------------------------------------------------
+-- esc properties (integration tests for Coq-extracted implementation)
+-- --------------------------------------------------------------------------
+
+prop_esc_empty :: Bool
+prop_esc_empty = esc T.empty == T.empty
+
+prop_esc_safe :: String -> Property
+prop_esc_safe s =
+    all (`notElem` ("<>&\"'" :: String)) s ==>
+    esc (T.pack s) == T.pack s
+
+prop_esc_no_raw_lt :: String -> Bool
+prop_esc_no_raw_lt s =
+    not (T.isInfixOf "<" (esc (T.pack s)))
+
+prop_esc_no_raw_gt :: String -> Bool
+prop_esc_no_raw_gt s =
+    not (T.isInfixOf ">" (esc (T.pack s)))
+
+prop_esc_no_raw_quot :: String -> Bool
+prop_esc_no_raw_quot s =
+    not (T.isInfixOf "\"" (esc (T.pack s)))
+
+-- --------------------------------------------------------------------------
+-- formatSize properties
+-- --------------------------------------------------------------------------
+
+prop_formatSize_has_unit :: NonNegative Int -> Bool
+prop_formatSize_has_unit (NonNegative n) =
+    let result = formatSize n
+    in T.isSuffixOf " B" result
+       || T.isSuffixOf " KiB" result
+       || T.isSuffixOf " MiB" result
+
+prop_formatSize_B :: NonNegative Int -> Property
+prop_formatSize_B (NonNegative n) =
+    n < 1024 ==> T.isSuffixOf " B" (formatSize n)
+
+prop_formatSize_KiB :: Property
+prop_formatSize_KiB =
+    forAll (choose (1024, 1048575)) $ \n ->
+    T.isSuffixOf " KiB" (formatSize n)
+
+prop_formatSize_MiB :: Property
+prop_formatSize_MiB =
+    forAll (choose (1048576, maxBound `div` 2)) $ \n ->
+    T.isSuffixOf " MiB" (formatSize (n :: Int))
+
+-- --------------------------------------------------------------------------
+-- shortAuthor properties
+-- --------------------------------------------------------------------------
+
+prop_shortAuthor_strips_email :: String -> String -> Property
+prop_shortAuthor_strips_email name email =
+    not (null name) && not (null email)
+    && all (/= '<') name ==>
+    let input = T.pack (name ++ " <" ++ email ++ ">")
+        result = shortAuthor input
+    in not (T.isInfixOf "<" result)
+
+prop_shortAuthor_preserves_plain :: String -> Property
+prop_shortAuthor_preserves_plain name =
+    notElem '<' name && not (null name) ==>
+    shortAuthor (T.pack name) == T.strip (T.pack name)
+
+-- --------------------------------------------------------------------------
+-- formatAbsolute properties
+-- --------------------------------------------------------------------------
+
+prop_formatAbsolute_short_unchanged :: String -> Property
+prop_formatAbsolute_short_unchanged s =
+    length s < 14 ==>
+    formatAbsolute (T.pack s) == T.pack s
+
+prop_formatAbsolute_long_has_separators :: Property
+prop_formatAbsolute_long_has_separators =
+    forAll genDateString $ \s ->
+      let result = formatAbsolute (T.pack s)
+      in T.isInfixOf "-" result && T.isInfixOf ":" result
+  where
+    genDateString = do
+      y <- choose (1970, 2099) :: Gen Int
+      mo <- choose (1, 12) :: Gen Int
+      d <- choose (1, 28) :: Gen Int
+      h <- choose (0, 23) :: Gen Int
+      mi <- choose (0, 59) :: Gen Int
+      se <- choose (0, 59) :: Gen Int
+      return $ pad 4 y ++ pad 2 mo ++ pad 2 d ++ pad 2 h ++ pad 2 mi ++ pad 2 se
+    pad n v = let s = show v in replicate (n - length s) '0' ++ s
+
+-- --------------------------------------------------------------------------
+-- highlightDiff properties
+-- --------------------------------------------------------------------------
+
+prop_highlightDiff_add_line :: String -> Bool
+prop_highlightDiff_add_line s =
+    let input = T.pack ("+" ++ s)
+        result = highlightDiff input
+    in T.isPrefixOf "<span class=\"diff-add\">" result
+
+prop_highlightDiff_del_line :: String -> Bool
+prop_highlightDiff_del_line s =
+    let input = T.pack ("-" ++ s)
+        result = highlightDiff input
+    in T.isPrefixOf "<span class=\"diff-del\">" result
+
+prop_highlightDiff_hunk_line :: String -> Bool
+prop_highlightDiff_hunk_line s =
+    let input = T.pack ("@@" ++ s)
+        result = highlightDiff input
+    in T.isPrefixOf "<span class=\"diff-hunk\">" result
+
+-- --------------------------------------------------------------------------
+-- Test runner
+-- --------------------------------------------------------------------------
+
+tests :: IO Bool
+tests = fmap and $ sequence
+    [ run "esc empty"                   (property prop_esc_empty)
+    , run "esc safe passthrough"        prop_esc_safe
+    , run "esc no raw <"               (property prop_esc_no_raw_lt)
+    , run "esc no raw >"               (property prop_esc_no_raw_gt)
+    , run "esc no raw \""              (property prop_esc_no_raw_quot)
+    , run "formatSize has unit"        (property prop_formatSize_has_unit)
+    , run "formatSize < 1024 ��� B"      prop_formatSize_B
+    , run "formatSize 1024..1M ��� KiB"  (property prop_formatSize_KiB)
+    , run "formatSize ��� 1M ��� MiB"      (property prop_formatSize_MiB)
+    , run "shortAuthor strips email"   prop_shortAuthor_strips_email
+    , run "shortAuthor plain"          prop_shortAuthor_preserves_plain
+    , run "formatAbsolute short"       prop_formatAbsolute_short_unchanged
+    , run "formatAbsolute separators"  (property prop_formatAbsolute_long_has_separators)
+    , run "highlightDiff + line"       (property prop_highlightDiff_add_line)
+    , run "highlightDiff - line"       (property prop_highlightDiff_del_line)
+    , run "highlightDiff @@ line"      (property prop_highlightDiff_hunk_line)
+    ]
+  where
+    run name prop = do
+      putStr $ "  " ++ name ++ ": "
+      r <- quickCheckWithResult stdArgs { maxSuccess = 200 } prop
+      return (isSuccess r)
addfile ./test/Spec.hs
hunk ./test/Spec.hs 1
+module Main where
+
+import System.Process (callCommand)
+import System.Exit (exitFailure, exitSuccess)
+import Control.Exception (try, SomeException)
+import qualified Properties.Html as Html
+import qualified Properties.Csp as Csp
+
+main :: IO ()
+main = do
+    -- Phase 1: Verify Rocq/Coq proofs
+    putStrLn "=== Verifying Rocq proofs ==="
+    proofResult <- try (callCommand "make -C verified proofs")
+                   :: IO (Either SomeException ())
+    case proofResult of
+      Left e -> do
+        putStrLn $ "Proof verification failed: " ++ show e
+        exitFailure
+      Right () ->
+        putStrLn "All proofs verified."
+
+    -- Phase 2: Run QuickCheck property tests
+    putStrLn "\n=== Running QuickCheck properties (HTML) ==="
+    htmlOk <- Html.tests
+
+    putStrLn "\n=== Running QuickCheck properties (CSP) ==="
+    cspOk <- Csp.tests
+
+    if htmlOk && cspOk
+      then do
+        putStrLn "\nAll properties passed."
+        exitSuccess
+      else do
+        putStrLn "\nSome properties FAILED."
+        exitFailure
adddir ./verified
addfile ./verified/Makefile
hunk ./verified/Makefile 1
+ROCQ = rocq c -Q . ""
+
+.PHONY: extract proofs clean all
+
+all: extract
+
+# -- Extraction targets --
+
+extract: ../gen/HtmlPure.hs ../gen/PathPure.hs ../gen/CspPure.hs
+
+../gen:
+	mkdir -p ../gen
+
+html_pure.vo ../gen/HtmlPure.hs: html_pure.v | ../gen
+	$(ROCQ) html_pure.v
+	@# Add GHC pragma and required imports for Haskell extraction
+	sed -i '1i{-# OPTIONS_GHC -w #-}' ../gen/HtmlPure.hs
+	sed -i '/^module.*where/a import qualified Data.Bits\nimport qualified Data.Char' ../gen/HtmlPure.hs
+
+path_pure.vo ../gen/PathPure.hs: path_pure.v | ../gen
+	$(ROCQ) path_pure.v
+	@# Add GHC pragma and required imports for Haskell extraction
+	sed -i '1i{-# OPTIONS_GHC -w #-}' ../gen/PathPure.hs
+	sed -i '/^module.*where/a import qualified Data.Bits\nimport qualified Data.Char' ../gen/PathPure.hs
+
+csp_pure.vo ../gen/CspPure.hs: csp_pure.v | ../gen
+	$(ROCQ) csp_pure.v
+	@# Add GHC pragma and required imports for Haskell extraction
+	sed -i '1i{-# OPTIONS_GHC -w #-}' ../gen/CspPure.hs
+	sed -i '/^module.*where/a import qualified Data.Bits\nimport qualified Data.Char' ../gen/CspPure.hs
+
+# -- Proof targets --
+
+proofs: html_pure_proofs.vo path_pure_proofs.vo csp_pure_proofs.vo
+
+html_pure_proofs.vo: html_pure_proofs.v html_pure.vo
+	$(ROCQ) html_pure_proofs.v
+
+path_pure_proofs.vo: path_pure_proofs.v path_pure.vo
+	$(ROCQ) path_pure_proofs.v
+
+csp_pure_proofs.vo: csp_pure_proofs.v csp_pure.vo
+	$(ROCQ) csp_pure_proofs.v
+
+# -- Clean --
+
+clean:
+	rm -f *.vo *.vok *.vos *.glob .*.aux
+	rm -f ../gen/HtmlPure.hs ../gen/PathPure.hs ../gen/CspPure.hs
addfile ./verified/csp_pure.v
hunk ./verified/csp_pure.v 1
+(** Verified pure functions for Content-Security-Policy header construction.
+    Extracted to Haskell for use in the DarcsWeb application.
+
+    Security property: the builder ensures no raw semicolons appear within
+    individual directive values, preventing CSP injection attacks where
+    an attacker-controlled value could introduce new directives. *)
+
+From Stdlib Require Import Ascii String Bool List.
+From Stdlib Require Import ExtrHaskellString.
+
+Import ListNotations.
+Open Scope string_scope.
+Open Scope bool_scope.
+
+(** -- Helper: check if a character appears in a string -- *)
+
+Fixpoint string_contains (needle : ascii) (haystack : string) : bool :=
+  match haystack with
+  | EmptyString => false
+  | String c rest => Ascii.eqb c needle || string_contains needle rest
+  end.
+
+(** -- Helper: remove all occurrences of a character -- *)
+
+Fixpoint strip_char (c : ascii) (s : string) : string :=
+  match s with
+  | EmptyString => EmptyString
+  | String h rest =>
+    if Ascii.eqb h c then strip_char c rest
+    else String h (strip_char c rest)
+  end.
+
+(** Sanitize a single CSP directive value by stripping semicolons. *)
+Definition sanitize_value (v : string) : string :=
+  strip_char ";"%char v.
+
+(** Build a single CSP directive: "name value".
+    The value is sanitized to strip any embedded semicolons. *)
+Definition build_directive (name : string) (value : string) : string :=
+  String.append name (String.append " " (sanitize_value value)).
+
+(** Join a list of strings with "; " separator. *)
+Fixpoint join_directives (ds : list string) : string :=
+  match ds with
+  | nil => EmptyString
+  | d :: nil => d
+  | d :: rest => String.append d (String.append "; " (join_directives rest))
+  end.
+
+(** Build a complete CSP header from a list of (name, value) pairs. *)
+Definition build_csp (directives : list (string * string)) : string :=
+  let ds := List.map (fun p => build_directive (fst p) (snd p)) directives in
+  join_directives ds.
+
+(* -- Extraction setup -- *)
+Set Extraction Output Directory "../gen".
+Extraction Language Haskell.
+
+Extract Inlined Constant String.append => "(Prelude.++)".
+
+Extraction "CspPure"
+  sanitize_value
+  build_directive
+  build_csp.
addfile ./verified/csp_pure_proofs.v
hunk ./verified/csp_pure_proofs.v 1
+(** Correctness proofs for CSP header construction functions.
+
+    Key security theorem: sanitize_value eliminates all semicolons,
+    so no injected value can break out of its directive. *)
+
+From Stdlib Require Import Ascii String Bool List.
+Require Import csp_pure.
+
+Import ListNotations.
+Open Scope string_scope.
+Open Scope bool_scope.
+
+(** -- strip_char correctness -- *)
+
+Lemma strip_char_empty : forall c, strip_char c "" = "".
+Proof. reflexivity. Qed.
+
+Lemma strip_char_removes : strip_char ";"%char "a;b" = "ab".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma strip_char_noop : strip_char ";"%char "abc" = "abc".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma strip_char_all : strip_char ";"%char ";;;" = "".
+Proof. vm_compute. reflexivity. Qed.
+
+(** -- Security theorem: sanitize_value strips all semicolons -- *)
+
+Lemma strip_char_no_target : forall c s,
+  string_contains c (strip_char c s) = false.
+Proof.
+  intros c s. induction s as [| h rest IH].
+  - reflexivity.
+  - simpl. destruct (Ascii.eqb h c) eqn:Heq.
+    + exact IH.
+    + simpl. rewrite Heq. simpl. exact IH.
+Qed.
+
+(** The key security property: sanitized values contain no semicolons. *)
+Theorem sanitize_value_no_semicolons : forall v,
+  string_contains ";"%char (sanitize_value v) = false.
+Proof.
+  intro v. unfold sanitize_value. apply strip_char_no_target.
+Qed.
+
+(** -- build_directive correctness -- *)
+
+Lemma build_directive_simple :
+  build_directive "default-src" "'none'" = "default-src 'none'".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma build_directive_sanitizes :
+  build_directive "style-src" "'self'; script-src 'unsafe-inline'" =
+  "style-src 'self' script-src 'unsafe-inline'".
+Proof. vm_compute. reflexivity. Qed.
+
+(** -- build_csp correctness -- *)
+
+Lemma build_csp_empty : build_csp nil = "".
+Proof. reflexivity. Qed.
+
+Lemma build_csp_single :
+  build_csp (("default-src", "'none'") :: nil) =
+  "default-src 'none'".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma build_csp_two :
+  build_csp (("default-src", "'none'") :: ("style-src", "'self'") :: nil) =
+  "default-src 'none'; style-src 'self'".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma build_csp_three :
+  build_csp (("default-src", "'none'") ::
+             ("style-src", "'self'") ::
+             ("img-src", "'self'") :: nil) =
+  "default-src 'none'; style-src 'self'; img-src 'self'".
+Proof. vm_compute. reflexivity. Qed.
+
+(** Injection attempt: semicolons in values are stripped. *)
+Lemma build_csp_injection_attempt :
+  build_csp (("default-src", "'none'; script-src 'unsafe-inline'") :: nil) =
+  "default-src 'none' script-src 'unsafe-inline'".
+Proof. vm_compute. reflexivity. Qed.
addfile ./verified/html_pure.v
hunk ./verified/html_pure.v 1
+(** Verified pure functions for HTML escaping.
+    Extracted to Haskell for use in the DarcsWeb application. *)
+
+From Stdlib.Strings Require Import Byte.
+From Stdlib Require Import Ascii String Bool.
+From Stdlib Require Import ExtrHaskellString.
+
+Open Scope string_scope.
+
+(* Characters that cannot be easily written as Coq string literals *)
+Definition dquote : ascii := Ascii.ascii_of_byte Byte.x22.
+Definition squote : ascii := Ascii.ascii_of_byte Byte.x27.
+
+(** HTML-escape a single character.
+    Replaces <, >, &, double-quote, single-quote with their HTML entity
+    equivalents. *)
+Definition esc_char (c : ascii) : string :=
+  if Ascii.eqb c "<"%char then "&lt;"
+  else if Ascii.eqb c ">"%char then "&gt;"
+  else if Ascii.eqb c "&"%char then "&amp;"
+  else if Ascii.eqb c dquote then "&quot;"
+  else if Ascii.eqb c squote then "&#39;"
+  else String c EmptyString.
+
+(** HTML-escape an entire string by escaping each character. *)
+Fixpoint esc (s : string) : string :=
+  match s with
+  | EmptyString => EmptyString
+  | String c rest => String.append (esc_char c) (esc rest)
+  end.
+
+(* -- Extraction setup -- *)
+Set Extraction Output Directory "../gen".
+Extraction Language Haskell.
+
+Extract Inlined Constant String.append => "(Prelude.++)".
+
+Extraction "HtmlPure" esc_char esc.
addfile ./verified/html_pure_proofs.v
hunk ./verified/html_pure_proofs.v 1
+(** Correctness proofs for HTML escaping functions. *)
+
+From Stdlib.Strings Require Import Byte.
+From Stdlib Require Import Ascii String Bool.
+Require Import html_pure.
+
+Open Scope string_scope.
+
+(** -- Concrete correctness for esc_char -- *)
+
+Lemma esc_char_lt : esc_char "<"%char = "&lt;".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma esc_char_gt : esc_char ">"%char = "&gt;".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma esc_char_amp : esc_char "&"%char = "&amp;".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma esc_char_quot : esc_char dquote = "&quot;".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma esc_char_apos : esc_char squote = "&#39;".
+Proof. vm_compute. reflexivity. Qed.
+
+(** Safe characters pass through unchanged *)
+
+Lemma esc_char_a : esc_char "a"%char = "a".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma esc_char_space : esc_char " "%char = " ".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma esc_char_zero : esc_char "0"%char = "0".
+Proof. vm_compute. reflexivity. Qed.
+
+(** -- String-level escaping -- *)
+
+Lemma esc_empty : esc EmptyString = EmptyString.
+Proof. reflexivity. Qed.
+
+Lemma esc_safe_string : esc "hello" = "hello".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma esc_lt_string : esc "<" = "&lt;".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma esc_mixed : esc "<b>" = "&lt;b&gt;".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma esc_amp_in_text : esc "a&b" = "a&amp;b".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma esc_script_tag : esc "<script>alert(1)</script>" =
+  "&lt;script&gt;alert(1)&lt;/script&gt;".
+Proof. vm_compute. reflexivity. Qed.
+
+(** -- Security property: esc output contains no raw '<' -- *)
+
+Fixpoint string_mem (c : ascii) (s : string) : bool :=
+  match s with
+  | EmptyString => false
+  | String c' rest => Ascii.eqb c c' || string_mem c rest
+  end.
+
+Lemma string_mem_append : forall c a b,
+  string_mem c (String.append a b) = string_mem c a || string_mem c b.
+Proof.
+  intros c a. induction a as [| c' a' IH]; intros b.
+  - reflexivity.
+  - simpl. rewrite IH. rewrite Bool.orb_assoc. reflexivity.
+Qed.
+
+(** No esc_char output contains a raw '<' character. *)
+Lemma esc_char_no_raw_lt : forall c, string_mem "<"%char (esc_char c) = false.
+Proof.
+  intro c.
+  destruct c as [[] [] [] [] [] [] [] []]; vm_compute; reflexivity.
+Qed.
+
+(** The key security theorem: escaping eliminates all raw '<' characters. *)
+Theorem esc_no_raw_lt : forall s, string_mem "<"%char (esc s) = false.
+Proof.
+  induction s as [| c rest IH].
+  - reflexivity.
+  - simpl. rewrite string_mem_append.
+    rewrite esc_char_no_raw_lt. simpl. exact IH.
+Qed.
+
+(** No esc_char output contains a raw '>' character. *)
+Lemma esc_char_no_raw_gt : forall c, string_mem ">"%char (esc_char c) = false.
+Proof.
+  intro c.
+  destruct c as [[] [] [] [] [] [] [] []]; vm_compute; reflexivity.
+Qed.
+
+(** Escaping eliminates all raw '>' characters. *)
+Theorem esc_no_raw_gt : forall s, string_mem ">"%char (esc s) = false.
+Proof.
+  induction s as [| c rest IH].
+  - reflexivity.
+  - simpl. rewrite string_mem_append.
+    rewrite esc_char_no_raw_gt. simpl. exact IH.
+Qed.
+
+(** No esc_char output contains a raw double-quote character. *)
+Lemma esc_char_no_raw_quot : forall c, string_mem dquote (esc_char c) = false.
+Proof.
+  intro c.
+  destruct c as [[] [] [] [] [] [] [] []]; vm_compute; reflexivity.
+Qed.
+
+(** Escaping eliminates all raw double-quote characters. *)
+Theorem esc_no_raw_quot : forall s, string_mem dquote (esc s) = false.
+Proof.
+  induction s as [| c rest IH].
+  - reflexivity.
+  - simpl. rewrite string_mem_append.
+    rewrite esc_char_no_raw_quot. simpl. exact IH.
+Qed.
addfile ./verified/path_pure.v
hunk ./verified/path_pure.v 1
+(** Verified pure functions for file path validation.
+    Extracted to Haskell for use in the DarcsWeb application. *)
+
+From Stdlib Require Import Ascii String Bool List.
+From Stdlib Require Import ExtrHaskellString.
+
+Import ListNotations.
+Open Scope string_scope.
+Open Scope bool_scope.
+
+(** -- Helper functions -- *)
+
+(** Check if a string is empty. *)
+Definition string_is_empty (s : string) : bool :=
+  match s with
+  | EmptyString => true
+  | _ => false
+  end.
+
+(** Remove '/' characters from a string. *)
+Fixpoint remove_slashes (s : string) : string :=
+  match s with
+  | EmptyString => EmptyString
+  | String c rest =>
+    if Ascii.eqb c "/"%char then remove_slashes rest
+    else String c (remove_slashes rest)
+  end.
+
+(** Check if a string starts with '.'. *)
+Definition starts_with_dot (s : string) : bool :=
+  match s with
+  | String c _ => Ascii.eqb c "."%char
+  | EmptyString => false
+  end.
+
+(** Get the last character of a string. *)
+Fixpoint last_char (s : string) : option ascii :=
+  match s with
+  | EmptyString => None
+  | String c EmptyString => Some c
+  | String _ rest => last_char rest
+  end.
+
+(** -- Split path -- *)
+
+(** Split a string on '/' into segments (accumulator-based). *)
+Fixpoint split_path_aux (acc : string) (s : string) {struct s} : list string :=
+  match s with
+  | EmptyString => acc :: nil
+  | String c rest =>
+    if Ascii.eqb c "/"%char then
+      acc :: split_path_aux EmptyString rest
+    else
+      split_path_aux (String.append acc (String c EmptyString)) rest
+  end.
+
+(** Split a file path on '/' separators. *)
+Definition split_path (s : string) : list string :=
+  match s with
+  | EmptyString => nil
+  | _ => split_path_aux EmptyString s
+  end.
+
+(** -- Safe subpath validation -- *)
+
+(** Filter out empty strings from a list. *)
+Fixpoint filter_nonempty (l : list string) : list string :=
+  match l with
+  | nil => nil
+  | x :: xs =>
+    if string_is_empty x then filter_nonempty xs
+    else x :: filter_nonempty xs
+  end.
+
+(** Check if all elements satisfy a predicate. *)
+Fixpoint all_true (f : string -> bool) (l : list string) : bool :=
+  match l with
+  | nil => true
+  | x :: xs => f x && all_true f xs
+  end.
+
+(** Check if a single path segment is safe. *)
+Definition is_safe_segment (seg : string) : bool :=
+  let name := remove_slashes seg in
+  negb (string_is_empty name)
+  && negb (String.eqb name "..")
+  && negb (String.eqb name ".")
+  && negb (String.eqb name "_darcs")
+  && negb (String.eqb name ".git")
+  && negb (starts_with_dot name).
+
+(** Check whether a subpath is safe (no hidden/internal segments). *)
+Definition is_safe_sub_path (sub : string) : bool :=
+  let segments := filter_nonempty (split_path sub) in
+  match segments with
+  | nil => false
+  | _ => all_true is_safe_segment segments
+  end.
+
+(** -- Trailing slash -- *)
+
+(** Ensure a path ends with exactly one '/'. *)
+Definition add_trailing_slash (s : string) : string :=
+  match s with
+  | EmptyString => "/"
+  | _ =>
+    match last_char s with
+    | Some c =>
+      if Ascii.eqb c "/"%char then s
+      else String.append s "/"
+    | None => "/"
+    end
+  end.
+
+(* -- Extraction setup -- *)
+Set Extraction Output Directory "../gen".
+Extraction Language Haskell.
+
+Extract Inlined Constant String.append => "(Prelude.++)".
+
+Extraction "PathPure"
+  split_path
+  is_safe_sub_path
+  add_trailing_slash.
addfile ./verified/path_pure_proofs.v
hunk ./verified/path_pure_proofs.v 1
+(** Correctness proofs for path validation functions. *)
+
+From Stdlib Require Import Ascii String Bool List.
+Require Import path_pure.
+
+Import ListNotations.
+Open Scope string_scope.
+Open Scope bool_scope.
+
+(** -- split_path -- *)
+
+Lemma split_path_empty : split_path "" = nil.
+Proof. reflexivity. Qed.
+
+Lemma split_path_single : split_path "a" = "a" :: nil.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma split_path_simple : split_path "a/b" = "a" :: "b" :: nil.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma split_path_three : split_path "src/main/hs" = "src" :: "main" :: "hs" :: nil.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma split_path_leading_slash : split_path "/foo" = "" :: "foo" :: nil.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma split_path_trailing_slash : split_path "foo/" = "foo" :: "" :: nil.
+Proof. vm_compute. reflexivity. Qed.
+
+(** -- is_safe_sub_path: rejection of dangerous paths -- *)
+
+Lemma safe_rejects_empty : is_safe_sub_path "" = false.
+Proof. reflexivity. Qed.
+
+Lemma safe_rejects_dotdot : is_safe_sub_path ".." = false.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma safe_rejects_dot : is_safe_sub_path "." = false.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma safe_rejects_darcs : is_safe_sub_path "_darcs" = false.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma safe_rejects_git : is_safe_sub_path ".git" = false.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma safe_rejects_hidden : is_safe_sub_path ".hidden" = false.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma safe_rejects_nested_dotdot : is_safe_sub_path "foo/../bar" = false.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma safe_rejects_darcs_nested : is_safe_sub_path "repo/_darcs/prefs" = false.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma safe_rejects_hidden_nested : is_safe_sub_path "src/.secret/file" = false.
+Proof. vm_compute. reflexivity. Qed.
+
+(** -- is_safe_sub_path: acceptance of legitimate paths -- *)
+
+Lemma safe_accepts_simple : is_safe_sub_path "src" = true.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma safe_accepts_nested : is_safe_sub_path "src/Main.hs" = true.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma safe_accepts_deep : is_safe_sub_path "src/DarcsWeb/Html.hs" = true.
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma safe_accepts_underscore : is_safe_sub_path "my_module/test" = true.
+Proof. vm_compute. reflexivity. Qed.
+
+(** -- add_trailing_slash -- *)
+
+Lemma trailing_slash_empty : add_trailing_slash "" = "/".
+Proof. reflexivity. Qed.
+
+Lemma trailing_slash_already : add_trailing_slash "/foo/" = "/foo/".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma trailing_slash_adds : add_trailing_slash "/foo" = "/foo/".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma trailing_slash_root : add_trailing_slash "/" = "/".
+Proof. vm_compute. reflexivity. Qed.
+
+Lemma trailing_slash_idempotent_example :
+  add_trailing_slash (add_trailing_slash "/home/repos") =
+  add_trailing_slash "/home/repos".
+Proof. vm_compute. reflexivity. Qed.