feat: add target-aware PV11 optimizations (ADR-032)

[satran004]

Summary

Implements ADR-032 as a stacked change on the ADR-031 compiler-target branch from PR #93.

• adds explicit optimizer levels: none, baseline, pv11-safe, and pv11-costed
• makes the reviewed pv11-safe profile the default while retaining explicit baseline for pre-ADR-032 lowering and script-byte reproduction
• keeps the existing plutus-v3-pv11-uplc-1.1.0 compilation target; no new target is introduced
• pins the exact cardano-node-11.0.1-plutus-v3-pv11 optimization cost profile and provenance
• ships default O1 DropList, O2 Case Bool, and O13 literal ExpModInteger lowering
• keeps pv11-costed explicit; no cost-profile-dependent rule becomes default
• adds a typed opaque JulcValue boundary and rejects native/Data mixing through assignments, equality, Data-backed containers/records, and external boundaries
• updates both Scalus dependencies to stable 1.1.0 and restores PV11 Case Bool language-level cross-checks
• records evidence and explicit semantic prerequisites for every deferred O1-O15 candidate
• exposes consistent optimization selection and reporting through compiler, CLI, Gradle, annotation processor, and MCP surfaces

Target selection answers whether generated UPLC is legal. Optimization level and cost profile answer whether a proven rewrite is enabled and profitable. Future compiler targets start with ADR-032 rules disabled and opt rules in only after legality, semantic equivalence, and target-specific cost evidence are established.

Default promotion and compatibility

pv11-safe is now the single named default for Java compilation, CLI, Gradle, annotation processing, and MCP compile/evaluate entry points. This changes only newly compiled artifacts; deployed scripts are unchanged. Select baseline explicitly to reproduce ADR-031 lowering and hashes.

Default compiler output may contain PV11-only Case Bool or DropList. ADR-030 deliberately keeps Java/Truffle raw language-only overloads on the PV10 compatibility default, so JuLC-owned compiler consumers propagate CompileResult.target().ledgerTarget() through CLI, MCP, playground, testkit, examples, JRL, blueprint, and verification evaluation paths. Commands evaluating arbitrary raw UPLC retain compatibility-mode behavior.

Scalus 1.1.0 now evaluates the generated Case Bool shape with the correct false/true branch order and selected-branch-only laziness. The Scalus adapter remains language-only and fails closed on JuLC's protocol-aware ledger-target SPI; it is not claimed as a ledger-cost authority. Cross-backend raw budget tests explicitly configure the same pinned profile on both VMs instead of comparing version-dependent built-in defaults.

The decompiler conservatively recovers PV11 Case Bool as a source conditional only when the untyped scrutinee is provably Boolean. Ambiguous two-branch SOP cases remain switches.

The legacy exact-artifact Blaster suite is explicitly pinned to baseline. During default-promotion review, its PV11-safe 353-byte smoke artifact remained compute-bound in Lean preprocessing beyond ten minutes, while the same suite completed in about 36 seconds on baseline. This is a proof-tool performance limitation, not a semantic mismatch. The suite remains SMT-VALID, but it is not claimed as formal coverage of PV11-safe until Case Bool preprocessing is practical.

Correctness and security gates

• O1 preserves Java receiver-before-count evaluation order even though DropList uses count-before-list builtin arguments.
• O2 uses the PV11 Bool constructor order [false, true] and differentially checks success, failure, and laziness paths; Scalus 1.1.0 now passes focused compatibility regressions.
• O13 folds only reference-successful all-literal calls. Compiler folding and Java/Truffle execution share one pinned semantic helper with the exact 8191-bit operand bounds, modulus-one shortcut order, and failure messages. Oversized and otherwise failing calls remain unfurled.
• Native Value and Data cannot be mixed implicitly. Assignments, equality, lists, optionals, records, recursive type graphs, compile-method arguments, and validator boundaries fail closed with stable JULC0041/JULC0042 diagnostics.
• Java and Truffle VMs agree on result or exact failure text and traces for benchmark fixtures.
• Aggregate tests include accepted, below-threshold, negative-drop, empty, over-drop, malformed-list, and malformed-head cases.
• The pre-existing 3,000-case property suite checks shared generic optimizer passes. O1, O2, and O13 are covered by their focused differential, boundary, failure, trace, aggregate, and cross-backend tests; the generic property suite is not presented as direct shipped-rule coverage.
• Public entry-point regressions assert the default profile and compiler-target handoff.

Measured evidence

Pinned profile: cardano-node-11.0.1-plutus-v3-pv11

Rewrite	FLAT bytes	CPU	Memory
O1 DropList, isolated milestone evidence	162 -> 109	3,886,301 -> 2,311,844	17,931 -> 10,864
O2 Case Bool, success	134 -> 117	2,251,555 -> 1,687,408	9,694 -> 7,591
O13 ExpMod literal	42 -> 6	3,406,498 -> 16,100	3,407 -> 200
Aggregate accepted path	169 -> 88	5,346,583 -> 1,935,936	19,605 -> 8,533
Aggregate empty-after-drop	169 -> 88	5,328,905 -> 1,111,835	23,070 -> 5,464

The aggregate malformed-list path is unchanged at CPU 643,521 and memory 3,796. Every aggregate row is non-increasing in CPU and memory.

Aggregate script hashes change deterministically:

• baseline: 3d1e9ac3561e68d3d0864705686adca6105ff5fc15f5a43e904de1f2
• pv11-safe: 2f2ea7f79a5dd083ed51e573dc247267ae7cb978ecc615692479c594

Detailed tables, outcomes, traces, boundary cases, and deferral rationale are in adr/evidence/ and the release notes.

Validation

• focused semantic, failure, trace, deterministic-hash, target-propagation, Native Value, Scalus Case, ExpMod boundary, and decompiler tests
• complete Java, Truffle, Scalus, compiler, core, stdlib, and cardano-client module suites
• reproducible :julc-benchmark:optimizationEvidence suite with pinned Java/Truffle budgets and hashes
• ./gradlew build --no-daemon after the review-corrections milestone: 217 tasks, successful
• optimizer property suite: 3,000 generated generic optimizer cases
• managed legacy exact-artifact verification on explicit baseline: SMT-VALID, all reviewed positive properties and negative controls established
• documentation npm run build: 32 pages, successful
• git diff --check integration/adr-031-compiler-target...HEAD

Milestone history

Each coherent phase was developed on a separate milestone branch, tested and reviewed against ADR invariants, and merged with a no-fast-forward milestone merge into this integration branch. Milestone 6 promotes the evidence-backed safe profile to the default and preserves explicit baseline compatibility. Corrective milestone 6b makes the legacy Blaster baseline pin explicit after CI exposed the proof-preprocessing boundary. Milestone 7 addresses the external review: Scalus 1.1.0 compatibility, exact ExpMod bounds in compiler and VMs, comprehensive Native Value/Data isolation, corrected verification claims, and full repository revalidation.

Related: #77, #94, #95, #96, #97, #98, #99, #100, #101, #102, #103, #104, #105, #106, #107, #108.

[satran004]

Milestone 6 is merged into the integration branch. pv11-safe is now the default across compiler, CLI, Gradle, annotation processor, and MCP surfaces; explicit baseline remains the rollback/reproduction path. Compiler-owned evaluators now carry CompileResult.target() so PV11-only Case Bool and DropList output is evaluated under the correct ledger target. The merged tree passes ./gradlew build --no-daemon (217 tasks), including 3,000 optimizer property cases, target-propagation regressions, and conservative PV11 decompiler coverage.

[satran004]

CI exposed a locked-artifact migration issue rather than a compiler test failure. Rebuilding the Blaster suite with the new default changed every proof artifact hash; attempting the PV11-safe smoke proof then kept Lean compute-bound beyond ten minutes. Corrective milestone 6b now pins this legacy exact-artifact suite explicitly to baseline, documents that it is not formal PV11-safe coverage, and preserves the existing locked artifacts/counterexample bindings. The exact managed CI command passes locally on the merged integration commit in about 36 seconds with SMT-VALID: all-properties-established. PV11-safe remains the product default and is gated by the dedicated differential VM, property, failure, trace, deterministic-hash, aggregate, and benchmark suites.

[satran004]

Milestone 7 addresses the review findings in merge commit 16e5e35:

• F1 + VM twin: one pinned ExpModInteger semantic helper now enforces the reference guard order and 8191-bit bounds in compiler folding and Java/Truffle execution; the four reported operands and modulus-one ordering have regressions.
• F2: Native Value/Data isolation now covers assignments, equality, JulcList/Optional, records, recursive type graphs, compileMethod arguments, and validator boundaries with JULC0041/JULC0042; final Data-codec/lowering checks fail closed.
• F3: the PR description now states that the 3,000-case property suite covers shared generic optimizer passes, not O1/O2/O13 directly.
• F4: Scalus is updated to stable 1.1.0 and passes focused Case Bool branch-order/laziness tests. It remains language-only and fails closed on the protocol-aware SPI; raw budget parity tests pin one explicit profile on both sides.
• Minor VM list tag comment corrected.

Validation: affected module suites, pinned optimizationEvidence benchmark, and ./gradlew build --no-daemon (217 tasks) all pass.