fix(proof): make offline Isabelle replay portable on Ubuntu

.github/workflows/ci.yml

@@ -38,10 +38,13 @@ jobs:
           key: isabelle-linux-x86-64-2025-2-a20a507bc7c1270d
       - name: Install proof sandbox
         run: |
-          if ! command -v bwrap >/dev/null 2>&1; then
+          if ! command -v bwrap >/dev/null 2>&1 || ! command -v fc-list >/dev/null 2>&1 || [ -z "$(fc-list --format='%{file}\n' | head -n 1)" ]; then
             sudo apt-get update
-            sudo apt-get install --no-install-recommends -y bubblewrap
+            sudo apt-get install --no-install-recommends -y bubblewrap fontconfig fonts-dejavu-core
           fi
+          test -d /etc/fonts
+          test -d /usr/share/fonts
+          test -n "$(fc-list --format='%{file}\n' | head -n 1)"
       - name: Acquire pinned Isabelle distribution
         run: uv run --project implementations/python --frozen python -m tools.isabelle_tool acquire
       - name: Resolve policy base revision

CONTRIBUTING.md

@@ -58,6 +58,26 @@ The full repository gate is:
 uv tool run --from 'nox[uv]==2026.4.10' nox -f noxfile.py -s verify
 ```
 
+That gate includes a `participant-opacity-proof` lane, which replays the pinned
+Isabelle proof offline. The lane runs on Linux x86_64 only. It needs
+`bubblewrap` to enforce the offline replay, and a fontconfig setup with at least
+one installed font, because Isabelle starts a JVM that will not run without one:
+
+```shell
+sudo apt-get install bubblewrap fontconfig fonts-dejavu-core
+```
+
+The proof tool checks this fontconfig runtime before entering the sandbox and
+reports a missing prerequisite separately from a kernel rejection. Run the
+gate on Linux, or rely on continuous integration, when your workstation is
+another platform.
+
+Some Linux security policies also deny unprivileged user or network namespaces.
+The proof tool reports that condition as unavailable bubblewrap isolation and
+does not retry without the network sandbox. Use an administrator-approved host
+policy for bubblewrap or rely on continuous integration; do not disable the
+offline boundary to make the lane pass.
+
 Run the change-aware local gate while iterating:
 
 ```shell

docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md

@@ -0,0 +1,52 @@
+# Issue 1109 / ASR-535 Isabelle Sandbox Portability
+
+Date: 2026-08-11
+
+Issue: #1109. Requirement: ASR-535. Related: #963.
+
+## Reproduced gap
+
+The checksum-pinned Isabelle2025-2 distribution was acquired on Ubuntu 24.04
+x86_64 and started inside the repository's bubblewrap network namespace. The
+kernel replay stopped before loading the fixed session with `Fontconfig head is
+null, check your fonts or fonts configuration`.
+
+The sandbox already exposes `/etc/fonts` and `/usr/share/fonts`, but creates an
+otherwise empty `/usr/share`. On Ubuntu releases where `/etc/fonts/conf.d`
+entries resolve into `/usr/share/fontconfig`, the fixed runtime allowlist omits
+data required by the pinned prover. Ubuntu 22.04 instead keeps that configuration
+under `/etc/fonts`, so `/usr/share/fontconfig` is a distribution-specific,
+optional path. A minimal Ubuntu image can also omit the fontconfig runtime
+entirely because the canonical workflow installs only bubblewrap. The result is
+host-image-dependent proof admission even though theorem sources and the prover
+archive are unchanged.
+
+## Decision
+
+Install bubblewrap and fontconfig as explicit canonical-runner prerequisites,
+require the cross-release `/etc/fonts` and `/usr/share/fonts` directories before
+sandbox entry, and add the optional `/usr/share/fontconfig` directory to the
+fixed, read-only system-runtime allowlist when the host provides it.
+Do not bind the host root, user home, repository workspace, network, ambient
+environment, or any mutable proof input. Existing paths remain conditional so
+minimal distributions without that directory keep the same command shape.
+
+The allowlist membership is covered by a focused regression, while the
+canonical Ubuntu 22.04 job replays the checksum-pinned archive under bubblewrap
+network isolation. Ubuntu 24.04 supplied the reproduced fontconfig layout, but
+is not the canonical replay host because its default namespace policy can deny
+bubblewrap setup. The proof evidence digest and theorem semantics must remain
+unchanged.
+
+If the host denies bubblewrap namespace setup, the runner must report a stable
+sandbox-unavailable error rather than classify pre-prover output as a kernel
+rejection. It must not retry with host networking. Ubuntu installations with
+restrictive unprivileged-user-namespace policy use an administrator-approved
+bubblewrap policy or the canonical CI host.
+
+## Nonclaims
+
+This repairs Linux distribution portability for the declared canonical proof
+lane. It does not make arbitrary Isabelle installations portable, authorize a
+different prover or archive, expand the theorem claim, or replace the existing
+checksum, resource, filesystem, and offline-execution controls.

docs/requirements/ASR-535/requirement.md

@@ -52,3 +52,5 @@ ADR-081 governs relation discipline and current tests provide bounded evidence,
 - IMPLEMENTS → PROOF `specs/formal/participant-semantics/isabelle/Participant_Opacity.thy` (Kernel-checked participant-opacity theorem)
 - TESTS → TEST `implementations/python/tests/test_issue_963_participant_opacity_proof.py` (Issue 963 participant-opacity proof integration tests)
 - VERIFIES → PROOF `specs/formal/participant-semantics/participant-opacity-proof-evidence.json` (Participant-opacity proof evidence record)
+- IMPLEMENTS → GITHUB_ISSUE `1109` (Make the offline Isabelle sandbox portable on Ubuntu)
+- DOCUMENTS → DOCUMENTATION `docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md` (Pinned proof-runtime allowlist decision)

implementations/python/tests/test_issue_1109_proof_workflow.py

@@ -0,0 +1,21 @@
+"""ASR-535 regression guard for the canonical proof sandbox setup."""
+
+from pathlib import Path
+
+import yaml
+
+REPO_ROOT = Path(__file__).resolve().parents[3]
+
+
+def test_canonical_workflow_installs_the_offline_proof_runtime() -> None:
+    workflow = yaml.safe_load((REPO_ROOT / ".github" / "workflows" / "ci.yml").read_text(encoding="utf-8"))
+    steps = workflow["jobs"]["verify"]["steps"]
+    proof_runtime = next(step["run"] for step in steps if step.get("name") == "Install proof sandbox")
+
+    assert "command -v bwrap" in proof_runtime
+    assert "command -v fc-list" in proof_runtime
+    assert "bubblewrap fontconfig fonts-dejavu-core" in proof_runtime
+    assert "test -d /etc/fonts" in proof_runtime
+    assert "test -d /usr/share/fonts" in proof_runtime
+    assert "test -n" in proof_runtime
+    assert "fc-list --format=" in proof_runtime

implementations/python/tests/test_issue_963_participant_opacity_proof.py

@@ -7,6 +7,7 @@
 import json
 from copy import deepcopy
 from pathlib import Path
+from types import SimpleNamespace
 from urllib.error import URLError
 
 import pytest
@@ -31,8 +32,12 @@
 )
 from tools.isabelle_tool import (
     ISABELLE_PROCESS_ADDRESS_SPACE_LIMIT_MIB,
+    ISABELLE_REQUIRED_FONTCONFIG_PATHS,
+    ISABELLE_SYSTEM_RUNTIME_PATHS,
+    _bubblewrap_setup_failed,
     _proof_process_limits,
     _proof_sandbox_command,
+    _require_fontconfig_runtime,
 )
 
 REPO_ROOT = Path(__file__).resolve().parents[3]
@@ -123,6 +128,118 @@ def test_proof_sandbox_exposes_only_fixed_inputs_runtime_and_private_state() ->
     assert command[-2:] == ["-D", "/workspace/session"]
 
 
+def test_proof_sandbox_allowlists_fontconfig_symlink_targets() -> None:
+    assert Path("/etc/fonts") in ISABELLE_SYSTEM_RUNTIME_PATHS
+    assert Path("/usr/share/fontconfig") in ISABELLE_SYSTEM_RUNTIME_PATHS
+    assert Path("/usr/share/fonts") in ISABELLE_SYSTEM_RUNTIME_PATHS
+    assert set(ISABELLE_REQUIRED_FONTCONFIG_PATHS) <= set(ISABELLE_SYSTEM_RUNTIME_PATHS)
+    assert Path("/usr/share/fontconfig") not in ISABELLE_REQUIRED_FONTCONFIG_PATHS
+
+
+def test_proof_runtime_requires_complete_fontconfig_data(tmp_path: Path) -> None:
+    existing = tuple(tmp_path / name for name in ("etc-fonts", "share-fontconfig", "share-fonts"))
+    for path in existing:
+        path.mkdir()
+
+    _require_fontconfig_runtime(existing, font_query=lambda: True)
+
+    existing[-1].rmdir()
+    with pytest.raises(isabelle_tool.IsabelleToolError, match="fontconfig runtime is required"):
+        _require_fontconfig_runtime(existing, font_query=lambda: True)
+
+
+def test_proof_runtime_requires_a_discoverable_font(tmp_path: Path) -> None:
+    existing = tuple(tmp_path / name for name in ("etc-fonts", "share-fonts"))
+    for path in existing:
+        path.mkdir()
+
+    with pytest.raises(isabelle_tool.IsabelleToolError, match="fontconfig runtime is required"):
+        _require_fontconfig_runtime(existing, font_query=lambda: False)
+
+
+def test_fontconfig_query_requires_a_successful_nonempty_listing(
+    monkeypatch: pytest.MonkeyPatch,
+    tmp_path: Path,
+) -> None:
+    font_list = tmp_path / "fc-list"
+    font_list.write_text("stub", encoding="ascii")
+    font_list.chmod(0o755)
+
+    monkeypatch.setattr(
+        isabelle_tool.subprocess,
+        "run",
+        lambda *_args, **_kwargs: SimpleNamespace(returncode=0, stdout=b"/usr/share/fonts/example.ttf\n"),
+    )
+    assert isabelle_tool._fontconfig_has_fonts(font_list) is True
+
+    monkeypatch.setattr(
+        isabelle_tool.subprocess,
+        "run",
+        lambda *_args, **_kwargs: SimpleNamespace(returncode=0, stdout=b""),
+    )
+    assert isabelle_tool._fontconfig_has_fonts(font_list) is False
+
+
+def test_proof_replay_checks_fontconfig_before_session_entry(
+    monkeypatch: pytest.MonkeyPatch,
+    tmp_path: Path,
+) -> None:
+    original_is_file = Path.is_file
+
+    def reject_missing_fontconfig() -> None:
+        raise isabelle_tool.IsabelleToolError("fontconfig test sentinel")
+
+    monkeypatch.setattr(isabelle_tool, "require_isabelle", lambda _repo_root: tmp_path)
+    monkeypatch.setattr(
+        Path,
+        "is_file",
+        lambda path: path == Path("/usr/bin/bwrap") or original_is_file(path),
+    )
+    monkeypatch.setattr(
+        isabelle_tool,
+        "_require_fontconfig_runtime",
+        reject_missing_fontconfig,
+    )
+
+    with pytest.raises(isabelle_tool.IsabelleToolError, match="fontconfig test sentinel"):
+        isabelle_tool.run_isabelle_build(tmp_path)
+
+
+def test_proof_replay_distinguishes_sandbox_setup_from_kernel_rejection(
+    monkeypatch: pytest.MonkeyPatch,
+    tmp_path: Path,
+) -> None:
+    session_root = tmp_path / isabelle_tool.ISABELLE_SESSION_RELATIVE_PATH
+    session_root.mkdir(parents=True)
+    original_is_file = Path.is_file
+
+    monkeypatch.setattr(isabelle_tool, "require_isabelle", lambda _repo_root: tmp_path / "isabelle")
+    monkeypatch.setattr(
+        Path,
+        "is_file",
+        lambda path: path == Path("/usr/bin/bwrap") or original_is_file(path),
+    )
+    monkeypatch.setattr(isabelle_tool, "_require_fontconfig_runtime", lambda: None)
+
+    def completed_with(output: bytes):
+        def fake_run(*_args: object, stdout: object, **_kwargs: object) -> SimpleNamespace:
+            stdout.write(output)
+            return SimpleNamespace(returncode=1)
+
+        return fake_run
+
+    assert _bubblewrap_setup_failed("  bwrap: loopback setup denied\n") is True
+    assert _bubblewrap_setup_failed("*** Isabelle theorem failure\n") is False
+
+    monkeypatch.setattr(isabelle_tool.subprocess, "run", completed_with(b"bwrap: network namespace denied\n"))
+    with pytest.raises(isabelle_tool.IsabelleToolError, match="bubblewrap network isolation is unavailable"):
+        isabelle_tool.run_isabelle_build(tmp_path)
+
+    monkeypatch.setattr(isabelle_tool.subprocess, "run", completed_with(b"*** Isabelle theorem failure\n"))
+    with pytest.raises(isabelle_tool.IsabelleToolError, match="Isabelle kernel rejected"):
+        isabelle_tool.run_isabelle_build(tmp_path)
+
+
 def test_proof_process_limit_enforces_per_process_address_space(monkeypatch: pytest.MonkeyPatch) -> None:
     calls: list[tuple[int, tuple[int, int]]] = []
     monkeypatch.setattr(isabelle_tool.resource, "setrlimit", lambda kind, limits: calls.append((kind, limits)))

specs/formal/participant-semantics/participant-opacity-proof-evidence.json

@@ -292,7 +292,7 @@
       },
       {
         "path": "tools/isabelle_tool.py",
-        "digest": "sha256:5100ea993e91b07bb3ac764642fd6ca110e477882b35aba5c49403f314133c85"
+        "digest": "sha256:64a6c3190e2116f760de09969f978240ab3582173cc3765b03fb596cf52cd7c1"
       }
     ]
   },

tools/isabelle_tool.py

@@ -11,6 +11,7 @@
 import sys
 import tarfile
 import tempfile
+from collections.abc import Callable
 from pathlib import Path
 from urllib.error import HTTPError, URLError
 from urllib.request import urlopen
@@ -31,6 +32,7 @@
 ISABELLE_ARCHIVE_BYTES = 1_228_480_874
 ISABELLE_SESSION = "Participant_Opacity"
 ISABELLE_SESSION_RELATIVE_PATH = Path("specs/formal/participant-semantics/isabelle")
+ISABELLE_LOCALE = "C.UTF-8"
 ISABELLE_BUILD_TIMEOUT_SECONDS = 600
 ISABELLE_OUTPUT_LIMIT_BYTES = 64 * 1024
 ISABELLE_FILE_LIMIT_BYTES = 4 * 1024 * 1024 * 1024
@@ -45,6 +47,7 @@
     Path("/usr/lib"),
     Path("/usr/lib64"),
     Path("/usr/share/locale"),
+    Path("/usr/share/fontconfig"),
     Path("/usr/share/fonts"),
     Path("/usr/share/zoneinfo"),
     Path("/lib"),
@@ -53,6 +56,12 @@
     Path("/etc/ld.so.cache"),
     Path("/var/cache/fontconfig"),
 )
+ISABELLE_REQUIRED_FONTCONFIG_PATHS = (
+    Path("/etc/fonts"),
+    Path("/usr/share/fonts"),
+)
+ISABELLE_FONTCONFIG_LIST = Path("/usr/bin/fc-list")
+ISABELLE_FONTCONFIG_QUERY_TIMEOUT_SECONDS = 10
 _DOWNLOAD_CHUNK_BYTES = 1024 * 1024
 
 
@@ -210,7 +219,7 @@ def expected_isabelle_result() -> dict[str, object]:
         "result": "kernel-checked",
         "network": "blocked-by-bubblewrap-network-namespace",
         "filesystem": "allowlisted-runtime-session-and-private-state-only",
-        "locale": "C.UTF-8",
+        "locale": ISABELLE_LOCALE,
         "platform_boundary": "linux-x86_64",
     }
     encoded = json.dumps(result, ensure_ascii=False, separators=(",", ":"), sort_keys=True).encode("utf-8")
@@ -287,10 +296,10 @@ def _proof_sandbox_command(
             "/state/isabelle-user",
             "--setenv",
             "LANG",
-            "C.UTF-8",
+            ISABELLE_LOCALE,
             "--setenv",
             "LC_ALL",
-            "C.UTF-8",
+            ISABELLE_LOCALE,
             "--setenv",
             "TZ",
             "UTC",
@@ -307,13 +316,51 @@ def _proof_sandbox_command(
     return command
 
 
+def _fontconfig_has_fonts(font_list: Path = ISABELLE_FONTCONFIG_LIST) -> bool:
+    """Return whether the fixed host fontconfig tool finds an installed font."""
+
+    if not font_list.is_file() or not os.access(font_list, os.X_OK):
+        return False
+    try:
+        completed = subprocess.run(
+            [str(font_list), "--format=%{file}\\n"],
+            stdin=subprocess.DEVNULL,
+            stdout=subprocess.PIPE,
+            stderr=subprocess.DEVNULL,
+            check=False,
+            timeout=ISABELLE_FONTCONFIG_QUERY_TIMEOUT_SECONDS,
+            env={"LANG": ISABELLE_LOCALE, "LC_ALL": ISABELLE_LOCALE},
+        )
+    except (OSError, subprocess.TimeoutExpired):
+        return False
+    return completed.returncode == 0 and bool(completed.stdout.strip())
+
+
+def _require_fontconfig_runtime(
+    paths: tuple[Path, ...] = ISABELLE_REQUIRED_FONTCONFIG_PATHS,
+    *,
+    font_query: Callable[[], bool] = _fontconfig_has_fonts,
+) -> None:
+    """Fail before sandbox entry when the pinned prover's font runtime is absent."""
+
+    if any(not path.is_dir() for path in paths) or not font_query():
+        raise IsabelleToolError("fontconfig runtime is required for offline proof replay")
+
+
+def _bubblewrap_setup_failed(output: str) -> bool:
+    """Return whether bubblewrap failed before the fixed prover could start."""
+
+    return output.lstrip().startswith("bwrap:")
+
+
 def run_isabelle_build(repo_root: Path = REPO_ROOT) -> dict[str, object]:
     """Kernel-check the fixed session in a network-isolated, bounded process."""
 
     home = require_isabelle(repo_root)
     bwrap = Path("/usr/bin/bwrap")
     if not bwrap.is_file():
         raise IsabelleToolError("bubblewrap is required to enforce offline proof replay")
+    _require_fontconfig_runtime()
     session_root = (repo_root / ISABELLE_SESSION_RELATIVE_PATH).resolve()
     if not session_root.is_dir() or repo_root.resolve() not in session_root.parents:
         raise IsabelleToolError("the fixed Isabelle session root is unavailable")
@@ -354,6 +401,8 @@ def run_isabelle_build(repo_root: Path = REPO_ROOT) -> dict[str, object]:
             raise IsabelleToolError("Isabelle proof replay exceeded its wall-time bound") from exc
         output = _read_bounded_output(output_path)
         if completed.returncode != 0:
+            if _bubblewrap_setup_failed(output):
+                raise IsabelleToolError("bubblewrap network isolation is unavailable for offline proof replay")
             failure_tail = output.strip()[-4096:]
             detail = f":\n{failure_tail}" if failure_tail else ""
             raise IsabelleToolError(f"Isabelle kernel rejected the fixed proof session{detail}")