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: 8c9365cad7d1d4610cca45cf3c91cbe9c8933a83.
• Exact PR head: a6c001130b2bbc0c956017ed0d5bb773fa98298c.
• All eight commits are patch-identical after the rebase onto test(coverage): enforce branch-aware 90% policy #1143; the rebased CI workflow retains test(coverage): enforce branch-aware 90% policy #1143's branch-aware coverage semantics and changes only the proof-sandbox installation step.
• 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 31680471016 passes canonical Ubuntu verification, including the pinned offline Isabelle replay, coverage upload, fuzzing, Docker integration, supply-chain scan, and dependent Sonar gate.
• Exact-head Docs, CodeQL, title, and GitGuardian checks pass.
• Sonar quality gate passes with 85.2% new-code coverage, 0 new violations, and 0.0% new-code 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.