A whole reading of the resident z3's tree was sealed HwShunt on a
declaration the code made itself: "this crate spawned the z3". That
covers nothing about what answers to `z3` on PATH. A wrapper that
forwards each goal to a z3 in a container, a VM or on another host reads
whole here (only the forwarding client is in the tree) while the decision
is charged elsewhere; the review's wrapper was sealed HwShunt about 50x
short of the work.
As jcp-gateway does for an upstream and sandbox-proof for a local engine,
the reading is now sealed only on the operator's declaration that the z3
it runs decides each goal in its own process tree:
Z3Server::declared_self_contained(bool), resident_z3_ladder(bool), and in
proof-cli PROOF_Z3_SELF_CONTAINED=1. Undeclared, the default, a reading
keeps the model figure with Modelled::NotDeclaredSelfContained beside any
gaps. The session now starts z3 from the first z3 on PATH resolved to an
absolute path (symlinks followed), and Z3EnergyAccount::z3 records that
binary: the declaration is about it.
The z3 tree tests declare their Homebrew z3 explicitly; a new test shows
an undeclared server seals ModelBased for a whole reading (it was HwShunt
before), and a unit test checks the recorded path against the shell's own
lookup. README and proof-cli docs say when T1 is read off hardware.
Co-Authored-By: Claude Opus 5.5 <[email protected]>
d7e3b81c03