From a4ee7e1b8556ae690675a34ed2ae048166aecf3d Mon Sep 17 00:00:00 2001
From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com>
Date: Wed, 12 Aug 2026 12:54:54 -0700
Subject: [PATCH 1/8] docs(proof): record Ubuntu sandbox portability preflight
 (#1109)

---
 ...09-asr-535-isabelle-sandbox-portability.md | 38 +++++++++++++++++++
 docs/requirements/ASR-535/requirement.md      |  2 +
 2 files changed, 40 insertions(+)
 create mode 100644 docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md

diff --git a/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
new file mode 100644
index 00000000..5cc56237
--- /dev/null
+++ b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
@@ -0,0 +1,38 @@
+# 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`. Ubuntu's `/etc/fonts/conf.d` entries resolve into
+`/usr/share/fontconfig`, so the fixed runtime allowlist omits data required by
+the pinned prover. The result is host-image-dependent proof admission even
+though theorem sources and the prover archive are unchanged.
+
+## Decision
+
+Add `/usr/share/fontconfig` to the fixed, read-only system-runtime allowlist.
+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. Acceptance also
+requires a real Ubuntu 24.04 x86_64 replay of the checksum-pinned archive under
+bubblewrap network isolation. The proof evidence digest and theorem semantics
+must remain unchanged.
+
+## 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.
+
diff --git a/docs/requirements/ASR-535/requirement.md b/docs/requirements/ASR-535/requirement.md
index b0d084ce..1f2f9fc6 100644
--- a/docs/requirements/ASR-535/requirement.md
+++ b/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)

From 63ed17e2eb1ac02caa403446394652b1bdc0f949 Mon Sep 17 00:00:00 2001
From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com>
Date: Wed, 12 Aug 2026 12:54:54 -0700
Subject: [PATCH 2/8] fix(proof): make offline replay portable on Ubuntu
 (#1109)

---
 .github/workflows/ci.yml                      |  7 ++-
 ...09-asr-535-isabelle-sandbox-portability.md | 11 ++--
 .../tests/test_issue_1109_proof_workflow.py   | 23 +++++++++
 ...est_issue_963_participant_opacity_proof.py | 50 ++++++++++++++++++-
 .../participant-opacity-proof-evidence.json   |  2 +-
 tools/isabelle_tool.py                        | 16 ++++++
 6 files changed, 101 insertions(+), 8 deletions(-)
 create mode 100644 implementations/python/tests/test_issue_1109_proof_workflow.py

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 40ad08a7..19d93609 100644
--- a/.github/workflows/ci.yml
+++ b/.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; then
             sudo apt-get update
-            sudo apt-get install --no-install-recommends -y bubblewrap
+            sudo apt-get install --no-install-recommends -y bubblewrap fontconfig
           fi
+          test -d /etc/fonts
+          test -d /usr/share/fontconfig
+          test -d /usr/share/fonts
       - name: Acquire pinned Isabelle distribution
         run: uv run --project implementations/python --frozen python -m tools.isabelle_tool acquire
       - name: Resolve policy base revision
diff --git a/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
index 5cc56237..4ce27630 100644
--- a/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
+++ b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
@@ -14,12 +14,16 @@ null, check your fonts or fonts configuration`.
 The sandbox already exposes `/etc/fonts` and `/usr/share/fonts`, but creates an
 otherwise empty `/usr/share`. Ubuntu's `/etc/fonts/conf.d` entries resolve into
 `/usr/share/fontconfig`, so the fixed runtime allowlist omits data required by
-the pinned prover. The result is host-image-dependent proof admission even
-though theorem sources and the prover archive are unchanged.
+the pinned prover. 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
 
-Add `/usr/share/fontconfig` to the fixed, read-only system-runtime allowlist.
+Install bubblewrap and fontconfig as explicit canonical-runner prerequisites,
+require the fixed fontconfig directories before sandbox entry, and add
+`/usr/share/fontconfig` to the fixed, read-only system-runtime allowlist.
 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.
@@ -35,4 +39,3 @@ 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.
-
diff --git a/implementations/python/tests/test_issue_1109_proof_workflow.py b/implementations/python/tests/test_issue_1109_proof_workflow.py
new file mode 100644
index 00000000..f196b10a
--- /dev/null
+++ b/implementations/python/tests/test_issue_1109_proof_workflow.py
@@ -0,0 +1,23 @@
+"""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" in proof_runtime
+    assert "test -d /etc/fonts" in proof_runtime
+    assert "test -d /usr/share/fontconfig" in proof_runtime
+    assert "test -d /usr/share/fonts" in proof_runtime
diff --git a/implementations/python/tests/test_issue_963_participant_opacity_proof.py b/implementations/python/tests/test_issue_963_participant_opacity_proof.py
index f6946830..81db0203 100644
--- a/implementations/python/tests/test_issue_963_participant_opacity_proof.py
+++ b/implementations/python/tests/test_issue_963_participant_opacity_proof.py
@@ -10,7 +10,6 @@
 from urllib.error import URLError
 
 import pytest
-import tools.isabelle_tool as isabelle_tool
 from jsonschema import Draft202012Validator
 from pydantic import ValidationError
 from raes_contracts.behavioral_relation_profiles import (
@@ -24,6 +23,8 @@
     load_behavioral_relation_catalog,
     load_behavioral_relation_catalog_revision,
 )
+
+import tools.isabelle_tool as isabelle_tool
 from tools.check_participant_opacity_proof import (
     ProofEvidenceError,
     load_proof_manifest,
@@ -31,8 +32,11 @@
 )
 from tools.isabelle_tool import (
     ISABELLE_PROCESS_ADDRESS_SPACE_LIMIT_MIB,
+    ISABELLE_REQUIRED_FONTCONFIG_PATHS,
+    ISABELLE_SYSTEM_RUNTIME_PATHS,
     _proof_process_limits,
     _proof_sandbox_command,
+    _require_fontconfig_runtime,
 )
 
 REPO_ROOT = Path(__file__).resolve().parents[3]
@@ -123,6 +127,50 @@ 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)
+
+
+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)
+
+    existing[-1].rmdir()
+    with pytest.raises(isabelle_tool.IsabelleToolError, match="fontconfig runtime is required"):
+        _require_fontconfig_runtime(existing)
+
+
+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_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)))
diff --git a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
index fc916be9..88e6b02c 100644
--- a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
+++ b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
@@ -292,7 +292,7 @@
       },
       {
         "path": "tools/isabelle_tool.py",
-        "digest": "sha256:5100ea993e91b07bb3ac764642fd6ca110e477882b35aba5c49403f314133c85"
+        "digest": "sha256:e7423efc782afe63e447f9fd6c8e2c33fc6210642ab47520a217a39661e405e8"
       }
     ]
   },
diff --git a/tools/isabelle_tool.py b/tools/isabelle_tool.py
index acc82e0b..2e5449f3 100644
--- a/tools/isabelle_tool.py
+++ b/tools/isabelle_tool.py
@@ -45,6 +45,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 +54,11 @@
     Path("/etc/ld.so.cache"),
     Path("/var/cache/fontconfig"),
 )
+ISABELLE_REQUIRED_FONTCONFIG_PATHS = (
+    Path("/etc/fonts"),
+    Path("/usr/share/fontconfig"),
+    Path("/usr/share/fonts"),
+)
 _DOWNLOAD_CHUNK_BYTES = 1024 * 1024
 
 
@@ -307,6 +313,15 @@ def _proof_sandbox_command(
     return command
 
 
+def _require_fontconfig_runtime(
+    paths: tuple[Path, ...] = ISABELLE_REQUIRED_FONTCONFIG_PATHS,
+) -> None:
+    """Fail before sandbox entry when the pinned prover's font runtime is absent."""
+
+    if any(not path.is_dir() for path in paths):
+        raise IsabelleToolError("fontconfig runtime is required for offline proof replay")
+
+
 def run_isabelle_build(repo_root: Path = REPO_ROOT) -> dict[str, object]:
     """Kernel-check the fixed session in a network-isolated, bounded process."""
 
@@ -314,6 +329,7 @@ def run_isabelle_build(repo_root: Path = REPO_ROOT) -> dict[str, object]:
     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")

From 615b243d7cdbe09ae94499c5382e67c402d936b8 Mon Sep 17 00:00:00 2001
From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com>
Date: Wed, 12 Aug 2026 12:54:54 -0700
Subject: [PATCH 3/8] docs(contributing): state proof runtime prerequisites
 (#1118, #1109)

---
 CONTRIBUTING.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index b82ab5a0..271fc1ac 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -58,6 +58,20 @@ 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.
+
 Run the change-aware local gate while iterating:
 
 ```shell

From 851251289c67520e2f81e6fd469a650851c28c5f Mon Sep 17 00:00:00 2001
From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com>
Date: Wed, 12 Aug 2026 12:54:54 -0700
Subject: [PATCH 4/8] fix(proof): distinguish sandbox setup failures (#1109)

---
 CONTRIBUTING.md                               |  6 +++
 ...09-asr-535-isabelle-sandbox-portability.md |  6 +++
 .../tests/test_issue_1109_proof_workflow.py   |  5 +--
 ...est_issue_963_participant_opacity_proof.py | 37 +++++++++++++++++++
 .../participant-opacity-proof-evidence.json   |  2 +-
 tools/isabelle_tool.py                        |  8 ++++
 6 files changed, 59 insertions(+), 5 deletions(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 271fc1ac..0dfc895f 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -72,6 +72,12 @@ 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
diff --git a/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
index 4ce27630..c8ba1da6 100644
--- a/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
+++ b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
@@ -33,6 +33,12 @@ requires a real Ubuntu 24.04 x86_64 replay of the checksum-pinned archive under
 bubblewrap network isolation. 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
diff --git a/implementations/python/tests/test_issue_1109_proof_workflow.py b/implementations/python/tests/test_issue_1109_proof_workflow.py
index f196b10a..5824b842 100644
--- a/implementations/python/tests/test_issue_1109_proof_workflow.py
+++ b/implementations/python/tests/test_issue_1109_proof_workflow.py
@@ -4,14 +4,11 @@
 
 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")
-    )
+    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")
 
diff --git a/implementations/python/tests/test_issue_963_participant_opacity_proof.py b/implementations/python/tests/test_issue_963_participant_opacity_proof.py
index 81db0203..71cbd71b 100644
--- a/implementations/python/tests/test_issue_963_participant_opacity_proof.py
+++ b/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
@@ -34,6 +35,7 @@
     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,
@@ -171,6 +173,41 @@ def reject_missing_fontconfig() -> None:
         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)))
diff --git a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
index 88e6b02c..c13bb967 100644
--- a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
+++ b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
@@ -292,7 +292,7 @@
       },
       {
         "path": "tools/isabelle_tool.py",
-        "digest": "sha256:e7423efc782afe63e447f9fd6c8e2c33fc6210642ab47520a217a39661e405e8"
+        "digest": "sha256:6d430acc5668c3fa693dc020314dadb55609496dd1545ac0ca164c84a6474b9b"
       }
     ]
   },
diff --git a/tools/isabelle_tool.py b/tools/isabelle_tool.py
index 2e5449f3..0e219310 100644
--- a/tools/isabelle_tool.py
+++ b/tools/isabelle_tool.py
@@ -322,6 +322,12 @@ def _require_fontconfig_runtime(
         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."""
 
@@ -370,6 +376,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}")

From c0084f265b845e184b7d69e65d2ff03e92741d8e Mon Sep 17 00:00:00 2001
From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com>
Date: Wed, 12 Aug 2026 13:25:15 -0700
Subject: [PATCH 5/8] fix(proof): support Ubuntu fontconfig layouts (#1109)

---
 .github/workflows/ci.yml                            |  1 -
 ...sue-1109-asr-535-isabelle-sandbox-portability.md | 13 ++++++++-----
 .../python/tests/test_issue_1109_proof_workflow.py  |  1 -
 .../test_issue_963_participant_opacity_proof.py     |  4 ++--
 .../participant-opacity-proof-evidence.json         |  2 +-
 tools/isabelle_tool.py                              |  1 -
 6 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 19d93609..3aee6326 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -43,7 +43,6 @@ jobs:
             sudo apt-get install --no-install-recommends -y bubblewrap fontconfig
           fi
           test -d /etc/fonts
-          test -d /usr/share/fontconfig
           test -d /usr/share/fonts
       - name: Acquire pinned Isabelle distribution
         run: uv run --project implementations/python --frozen python -m tools.isabelle_tool acquire
diff --git a/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
index c8ba1da6..0baf1b63 100644
--- a/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
+++ b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
@@ -12,9 +12,11 @@ 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`. Ubuntu's `/etc/fonts/conf.d` entries resolve into
-`/usr/share/fontconfig`, so the fixed runtime allowlist omits data required by
-the pinned prover. A minimal Ubuntu image can also omit the fontconfig runtime
+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.
@@ -22,8 +24,9 @@ archive are unchanged.
 ## Decision
 
 Install bubblewrap and fontconfig as explicit canonical-runner prerequisites,
-require the fixed fontconfig directories before sandbox entry, and add
-`/usr/share/fontconfig` to the fixed, read-only system-runtime allowlist.
+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.
diff --git a/implementations/python/tests/test_issue_1109_proof_workflow.py b/implementations/python/tests/test_issue_1109_proof_workflow.py
index 5824b842..05fcb740 100644
--- a/implementations/python/tests/test_issue_1109_proof_workflow.py
+++ b/implementations/python/tests/test_issue_1109_proof_workflow.py
@@ -16,5 +16,4 @@ def test_canonical_workflow_installs_the_offline_proof_runtime() -> None:
     assert "command -v fc-list" in proof_runtime
     assert "bubblewrap fontconfig" in proof_runtime
     assert "test -d /etc/fonts" in proof_runtime
-    assert "test -d /usr/share/fontconfig" in proof_runtime
     assert "test -d /usr/share/fonts" in proof_runtime
diff --git a/implementations/python/tests/test_issue_963_participant_opacity_proof.py b/implementations/python/tests/test_issue_963_participant_opacity_proof.py
index 71cbd71b..94c2c6c4 100644
--- a/implementations/python/tests/test_issue_963_participant_opacity_proof.py
+++ b/implementations/python/tests/test_issue_963_participant_opacity_proof.py
@@ -11,6 +11,7 @@
 from urllib.error import URLError
 
 import pytest
+import tools.isabelle_tool as isabelle_tool
 from jsonschema import Draft202012Validator
 from pydantic import ValidationError
 from raes_contracts.behavioral_relation_profiles import (
@@ -24,8 +25,6 @@
     load_behavioral_relation_catalog,
     load_behavioral_relation_catalog_revision,
 )
-
-import tools.isabelle_tool as isabelle_tool
 from tools.check_participant_opacity_proof import (
     ProofEvidenceError,
     load_proof_manifest,
@@ -134,6 +133,7 @@ def test_proof_sandbox_allowlists_fontconfig_symlink_targets() -> None:
     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:
diff --git a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
index c13bb967..3fa5fbb8 100644
--- a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
+++ b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
@@ -292,7 +292,7 @@
       },
       {
         "path": "tools/isabelle_tool.py",
-        "digest": "sha256:6d430acc5668c3fa693dc020314dadb55609496dd1545ac0ca164c84a6474b9b"
+        "digest": "sha256:79e7aba6d7eb9d449cd524fde9db70759bd3812a5a24d1990413558d704c8cf1"
       }
     ]
   },
diff --git a/tools/isabelle_tool.py b/tools/isabelle_tool.py
index 0e219310..e5dcddb5 100644
--- a/tools/isabelle_tool.py
+++ b/tools/isabelle_tool.py
@@ -56,7 +56,6 @@
 )
 ISABELLE_REQUIRED_FONTCONFIG_PATHS = (
     Path("/etc/fonts"),
-    Path("/usr/share/fontconfig"),
     Path("/usr/share/fonts"),
 )
 _DOWNLOAD_CHUNK_BYTES = 1024 * 1024

From 98921dc86c462e89b92f636e700038f584d87289 Mon Sep 17 00:00:00 2001
From: Brad Edwards <j.bradley.edwards@gmail.com>
Date: Thu, 13 Aug 2026 05:28:17 +0200
Subject: [PATCH 6/8] fix(proof): validate installed font runtime

---
 .github/workflows/ci.yml                      |  5 ++-
 ...09-asr-535-isabelle-sandbox-portability.md | 10 +++--
 .../tests/test_issue_1109_proof_workflow.py   |  4 +-
 ...est_issue_963_participant_opacity_proof.py | 39 +++++++++++++++++--
 .../participant-opacity-proof-evidence.json   |  2 +-
 tools/isabelle_tool.py                        | 27 ++++++++++++-
 6 files changed, 75 insertions(+), 12 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 3aee6326..87f382b7 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -38,12 +38,13 @@ jobs:
           key: isabelle-linux-x86-64-2025-2-a20a507bc7c1270d
       - name: Install proof sandbox
         run: |
-          if ! command -v bwrap >/dev/null 2>&1 || ! command -v fc-list >/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 fontconfig
+            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
diff --git a/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
index 0baf1b63..2c1b0e6e 100644
--- a/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
+++ b/docs/decisions/issue-1109-asr-535-isabelle-sandbox-portability.md
@@ -31,10 +31,12 @@ 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. Acceptance also
-requires a real Ubuntu 24.04 x86_64 replay of the checksum-pinned archive under
-bubblewrap network isolation. The proof evidence digest and theorem semantics
-must remain unchanged.
+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
diff --git a/implementations/python/tests/test_issue_1109_proof_workflow.py b/implementations/python/tests/test_issue_1109_proof_workflow.py
index 05fcb740..d14aae55 100644
--- a/implementations/python/tests/test_issue_1109_proof_workflow.py
+++ b/implementations/python/tests/test_issue_1109_proof_workflow.py
@@ -14,6 +14,8 @@ def test_canonical_workflow_installs_the_offline_proof_runtime() -> None:
 
     assert "command -v bwrap" in proof_runtime
     assert "command -v fc-list" in proof_runtime
-    assert "bubblewrap fontconfig" 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
diff --git a/implementations/python/tests/test_issue_963_participant_opacity_proof.py b/implementations/python/tests/test_issue_963_participant_opacity_proof.py
index 94c2c6c4..a2f206e5 100644
--- a/implementations/python/tests/test_issue_963_participant_opacity_proof.py
+++ b/implementations/python/tests/test_issue_963_participant_opacity_proof.py
@@ -11,7 +11,6 @@
 from urllib.error import URLError
 
 import pytest
-import tools.isabelle_tool as isabelle_tool
 from jsonschema import Draft202012Validator
 from pydantic import ValidationError
 from raes_contracts.behavioral_relation_profiles import (
@@ -25,6 +24,8 @@
     load_behavioral_relation_catalog,
     load_behavioral_relation_catalog_revision,
 )
+
+import tools.isabelle_tool as isabelle_tool
 from tools.check_participant_opacity_proof import (
     ProofEvidenceError,
     load_proof_manifest,
@@ -141,11 +142,43 @@ def test_proof_runtime_requires_complete_fontconfig_data(tmp_path: Path) -> None
     for path in existing:
         path.mkdir()
 
-    _require_fontconfig_runtime(existing)
+    _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)
+        _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(
diff --git a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
index 3fa5fbb8..4a7960f6 100644
--- a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
+++ b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
@@ -292,7 +292,7 @@
       },
       {
         "path": "tools/isabelle_tool.py",
-        "digest": "sha256:79e7aba6d7eb9d449cd524fde9db70759bd3812a5a24d1990413558d704c8cf1"
+        "digest": "sha256:498b7ca8eb8122ef55e96553b980d5286f46aaaef2a98fa83e8ca930531e57ee"
       }
     ]
   },
diff --git a/tools/isabelle_tool.py b/tools/isabelle_tool.py
index e5dcddb5..8da69310 100644
--- a/tools/isabelle_tool.py
+++ b/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
@@ -58,6 +59,8 @@
     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
 
 
@@ -312,12 +315,34 @@ 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(  # noqa: S603 - fixed system tool and argv
+            [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": "C.UTF-8", "LC_ALL": "C.UTF-8"},
+        )
+    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):
+    if any(not path.is_dir() for path in paths) or not font_query():
         raise IsabelleToolError("fontconfig runtime is required for offline proof replay")
 
 

From 020ec45d010cdc379c9bf1443425d756dbd36b83 Mon Sep 17 00:00:00 2001
From: Brad Edwards <j.bradley.edwards@gmail.com>
Date: Thu, 13 Aug 2026 05:41:44 +0200
Subject: [PATCH 7/8] test(proof): normalize proof test imports

---
 .../python/tests/test_issue_963_participant_opacity_proof.py   | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/implementations/python/tests/test_issue_963_participant_opacity_proof.py b/implementations/python/tests/test_issue_963_participant_opacity_proof.py
index a2f206e5..ce066d89 100644
--- a/implementations/python/tests/test_issue_963_participant_opacity_proof.py
+++ b/implementations/python/tests/test_issue_963_participant_opacity_proof.py
@@ -11,6 +11,7 @@
 from urllib.error import URLError
 
 import pytest
+import tools.isabelle_tool as isabelle_tool
 from jsonschema import Draft202012Validator
 from pydantic import ValidationError
 from raes_contracts.behavioral_relation_profiles import (
@@ -24,8 +25,6 @@
     load_behavioral_relation_catalog,
     load_behavioral_relation_catalog_revision,
 )
-
-import tools.isabelle_tool as isabelle_tool
 from tools.check_participant_opacity_proof import (
     ProofEvidenceError,
     load_proof_manifest,

From a6c001130b2bbc0c956017ed0d5bb773fa98298c Mon Sep 17 00:00:00 2001
From: Yernat Yestekov <2068106+doublewhy@users.noreply.github.com>
Date: Wed, 12 Aug 2026 21:00:18 -0700
Subject: [PATCH 8/8] refactor(proof): centralize pinned replay locale (#1109)

---
 .../participant-opacity-proof-evidence.json           |  2 +-
 tools/isabelle_tool.py                                | 11 ++++++-----
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
index 4a7960f6..c1541725 100644
--- a/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
+++ b/specs/formal/participant-semantics/participant-opacity-proof-evidence.json
@@ -292,7 +292,7 @@
       },
       {
         "path": "tools/isabelle_tool.py",
-        "digest": "sha256:498b7ca8eb8122ef55e96553b980d5286f46aaaef2a98fa83e8ca930531e57ee"
+        "digest": "sha256:64a6c3190e2116f760de09969f978240ab3582173cc3765b03fb596cf52cd7c1"
       }
     ]
   },
diff --git a/tools/isabelle_tool.py b/tools/isabelle_tool.py
index 8da69310..ff976a51 100644
--- a/tools/isabelle_tool.py
+++ b/tools/isabelle_tool.py
@@ -32,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
@@ -218,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")
@@ -295,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",
@@ -321,14 +322,14 @@ def _fontconfig_has_fonts(font_list: Path = ISABELLE_FONTCONFIG_LIST) -> bool:
     if not font_list.is_file() or not os.access(font_list, os.X_OK):
         return False
     try:
-        completed = subprocess.run(  # noqa: S603 - fixed system tool and argv
+        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": "C.UTF-8", "LC_ALL": "C.UTF-8"},
+            env={"LANG": ISABELLE_LOCALE, "LC_ALL": ISABELLE_LOCALE},
         )
     except (OSError, subprocess.TimeoutExpired):
         return False