Repository navigation
fix(proof): make the offline Isabelle sandbox portable on Ubuntu #1109
Description
Requirement: ASR-535
Observed on a clean Ubuntu 24.04 x86_64 GCE verifier using the repository-pinned Isabelle2025-2 archive and bubblewrap 0.9.0. After bubblewrap network isolation was established, tools.isabelle_tool verify failed before theorem replay with: Fontconfig head is null, check your fonts or fonts configuration.
Root cause: the sandbox binds /etc/fonts and /usr/share/fonts but creates an otherwise empty /usr/share. Ubuntu fontconfig files under /etc/fonts/conf.d point into /usr/share/fontconfig, which is not in ISABELLE_SYSTEM_RUNTIME_PATHS. The declared allowlist is therefore incomplete and the canonical proof lane is host-image dependent.
Acceptance:
- Bind the minimum fixed fontconfig data path needed by the pinned prover, without binding host root, user home, or enabling network.
- Validate allowlist construction with focused line and branch coverage.
- Replay the pinned proof successfully on Ubuntu 24.04 x86_64 with bubblewrap network isolation.
- Preserve checksum verification, fixed argv/environment, bounded resources, and evidence digest behavior.
- Document the operational portability boundary and exact verification evidence.
This is core OpenRAE proof-gate reliability; it does not change theorem semantics or experiment code.
Activity
doublewhy commentedon Aug 12, 2026
Implemented locally (not pushed) in f8023174 and 8a04cee1. Focused Python tests: 22 passed; changed tools/isabelle_tool.py lines and branches: 100%; Ruff and repository policy: pass; requirement governance attempted but the configured Ground Control host was unavailable. Real Ubuntu 24.04 x86_64 replay used the checksum-pinned Isabelle2025-2 archive under bubblewrap network isolation and returned kernel-checked for Participant_Opacity with unchanged result digest sha256:6ad5778c78667a992cca5b958ebc0764f8880115de4ac2f99f22ec6883400325. The complete tools.check_participant_opacity_proof validator then reported participant-opacity-proof: verified. The branch is clean and unpushed.
doublewhy commentedon Aug 12, 2026
Follow-up 61643f99 now distinguishes host sandbox setup from theorem rejection. On the same Ubuntu 24.04 verifier, the normal unprivileged command fails closed with the exact stable diagnostic
bubblewrap network isolation is unavailable for offline proof replayunder the host AppArmor restriction; it does not retry without isolation. An isolated privileged replay still completes the full repository proof validator asparticipant-opacity-proof: verifiedwith the unchanged kernel result digest. Focused total is now 23 tests, and all newly changed tool lines/branches remain 100% covered.fix(proof): support Ubuntu fontconfig layouts (#1109)
fix(proof): support Ubuntu fontconfig layouts (#1109)
fix(proof): support Ubuntu fontconfig layouts (#1109)
docs(proof): record Ubuntu sandbox portability preflight (#1109)
fix(proof): make offline replay portable on Ubuntu (#1109)
docs(contributing): state proof runtime prerequisites (#1118, #1109)
fix(proof): distinguish sandbox setup failures (#1109)
fix(proof): support Ubuntu fontconfig layouts (#1109)
refactor(proof): centralize pinned replay locale (#1109)
docs(proof): record Ubuntu sandbox portability preflight (#1109)
fix(proof): make offline replay portable on Ubuntu (#1109)
docs(contributing): state proof runtime prerequisites (#1118, #1109)
fix(proof): distinguish sandbox setup failures (#1109)
fix(proof): support Ubuntu fontconfig layouts (#1109)
refactor(proof): centralize pinned replay locale (#1109)
fix(proof): make offline Isabelle replay portable on Ubuntu (#1131)
doublewhy commentedon Aug 13, 2026
Completed by #1131, squash-merged to
devas990e8fbc246769fd95f4100e225a2eb69e2812f3. Exact-head Ubuntu verification included the pinned offline Isabelle proof lane; all required checks and Sonar passed. Closing manually because merges to non-defaultdevdo not trigger GitHub closing keywords.