feat(verification): add experimental typed property DSL

[satran004]

Summary

Implements ADR-016 milestones E.1 through E.3:

• inventories and compatibility-gates the pinned CardanoLedgerApiBlaster surface;
• adds a closed, typed, versioned property AST and deterministic Lean lowering;
• generates contract-specific Java metamodels from compiler-owned ContractSchema;
• executes trusted property builders in a bounded worker and revalidates their canonical IR in the parent process;
• proves annotation/DSL semantic equivalence for @RequiresSigner; and
• adds an exact-UPLC seller-payment vertical slice with positive, refuted, vacuous, and multi-satisfaction controls.

Trust and scope

• The API is experimental and not yet stable.
• The DSL worker executes trusted project Java; process bounds are not an OS security sandbox.
• Candidate IR cannot introduce raw Lean and is validated against the closed node/type inventory.
• E.3 admits one reviewed seller-payment shape rather than arbitrary user predicates.
• The local payment property deliberately does not claim global multi-input/output protection.
• Verification metadata remains outside core lowering and has zero effect on validator UPLC.

Evidence

• E.1 capability revision/signature compatibility gate
• E.2 typed AST, canonical codec, worker protocol, invalid-composition, and annotation-equivalence tests
• E.3 authorized, unpaid, vacuous, and multi-satisfaction fixtures
• Exact artifact/hash, ledger-domain bridge, generated-source, non-vacuity, and certificate bindings

Follow-up

• E.3 was refreshed against compiler-owned strict-data-v1; handwritten raw-shape checks were removed and all four classifications were reproduced.
• E.4 expands purposes one reviewed slice at a time, beginning with minting.
• Hosted execution of untrusted property builders remains out of scope until an OS-level isolation design is accepted.

See adr/verification/016-typed-verification-dsl-and-profile-catalog.md.