[Wenbobobo]

Outcome

Adds an image-owned facade that accepts the existing OciVerifierExecutionPolicyV2 compile/query argv and emits the unchanged standard single-record result after substrate-specific rich checks pass.

Trust boundary

• no contract, control-plane, gateway, or OciLeanRunner special case
• compile and query remain separate; the host runner owns stop/seal/hash/read-only handoff
• wrapper, query helper, profile, source/runtime checksum manifests, actual OLean closure, and receipt are build-input bound
• success stdout is exactly one standard V2 record
• failure stdout is forbidden; stderr has a fixed prefix and a 4096-byte child diagnostic cap

This is a local V2-compatible preflight, not real fixed-image OciLeanRunner vertical evidence, admission, gateway authority, or T6.

Adversarial evidence

Each rejection binds source hash, exact phase, return code, and reason marker:

• compositional target dependency: compile/20 (Targets/DerivSound.olean)
• direct target import: compile/20 (Targets/ClosedSound.olean)
• statement replacement (Candidate : True): compile succeeds, query/21 rejects the canonical type

Verification

• two independent reviews; final: no P0-P3, merge
• full Python/policy: 781 passed, 12 skipped
• Dashboard: 15/15 and production build
• post-rebase focused: 45 passed; Ruff/format/diff and four shell syntax checks pass
• fixed digest verify, independent canary, and facade canary pass
• RecordingHarness covers full policy argv, compile, seal, query, and record parsing

Image: autolean/library-substrate@sha256:bc336196592536658395ff0867f3008fc256dc6a3fd9098f414e118f18d5d1ef

Raw receipt: f98010e0c4efb3a43a06bb7782507aa74e799e10822c0cecba890a858e8590df