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

[doublewhy]

Plain summary

Context

OpenRAE replays a checksum-pinned Isabelle proof inside an offline Bubblewrap sandbox. That CI lane independently checks the participant-opacity theorem without trusting a developer workstation or permitting network access during replay.

Problem

Isabelle starts a JVM that needs a working host fontconfig runtime. The sandbox did not expose one Ubuntu fontconfig location, the CI job did not guarantee that fontconfig and a font were installed, and Bubblewrap setup failures could be mislabeled as rejected mathematics. Contributors also lacked a clear statement of the supported proof host and prerequisites.

Fix

Install and validate the minimum font runtime in the Ubuntu proof job, mount only the required fontconfig paths read-only, fail before replay when fonts are unavailable, classify Bubblewrap setup failures separately from Isabelle kernel failures, and document the Linux x86_64 boundary. The checksum, fixed command/environment, resource bounds, and offline network isolation remain unchanged.

Issues closed

• Closes fix(proof): make the offline Isabelle sandbox portable on Ubuntu #1109 — proof-tool and Ubuntu sandbox portability.
• Closes docs: document offline proof lane platform and font prerequisites #1118 — contributor documentation for the proof lane prerequisites.

What changed

• Installs bubblewrap, fontconfig, and fonts-dejavu-core when the canonical runner lacks them.
• Verifies /etc/fonts, /usr/share/fonts, and a nonempty fc-list result before proof acquisition and replay.
• Adds the optional cross-Ubuntu /usr/share/fontconfig target to the fixed read-only sandbox allowlist.
• Reports missing font prerequisites and Bubblewrap namespace/setup failures with stable operational errors instead of calling them kernel rejection.
• Documents the supported host, namespace-policy boundary, and the rule that offline isolation must not be weakened.
• Uses one constant for the pinned C.UTF-8 replay locale and keeps the proof-evidence digest bound to the exact tool source.

Verification

• Exact dev base: 96b20ae8422fae9936bae928bbd8a1c14d2001da.
• Exact PR head: da4a3d7535e3b50ae1d22884796a398357e1038d.
• The original seven commits are patch-identical after rebase; the eighth commit contains only the behavior-preserving Sonar cleanup and proof-tool digest refresh.
• Local focused proof-tool and workflow suite: 17 passed.
• Local Ruff, changed-file hygiene, repository policy, workflow parsing, documentation, and full static policy/lint graph pass.
• Exact-head CI run 31665642582 passes canonical Ubuntu verification, including the pinned offline Isabelle replay, coverage upload, fuzzing, Docker integration, and supply-chain scan.
• Exact-head Docs, CodeQL, title, and GitGuardian checks pass.
• Sonar quality gate passes with 85.7% new-code coverage, 0 new violations, 0 bugs, 0 vulnerabilities, and 0.0% duplication.

Platform note

The actual Isabelle replay requires the pinned Linux x86_64 distribution and Bubblewrap. The canonical Ubuntu CI result above is the authoritative replay evidence; non-Linux contributors can still run the deterministic focused and policy checks locally.