Verification DSL roadmap: ADR-016 E.1–E.6

[satran004]

Purpose

Track the experimental typed verification DSL described by ADR-016. This is a roadmap issue, not a claim that the API or the entire Cardano ledger model is supported. Individual implementation slices should get their own sub-ADR or focused issue before development.

Implemented in PR #86

• E.1 — Capability inventory
  • Pinned CardanoLedgerApiBlaster revision and normalized signature gate.
  • Capability states distinguish TYPED, RAW_DATA_ONLY, UNSUPPORTED_IR, UNSUPPORTED_SOLVER, and upstream/model gaps.
• E.2 — Minimal typed AST prototype
  • Closed sealed typed AST and canonical schema-1 IR.
  • Contract metamodel generated from compiler-owned ContractSchema.
  • Bounded separate-JVM worker and authoritative parent-process validation.
  • Deterministic Lean rendering and equivalence with @RequiresSigner.
  • Non-integer raw literal injection rejected at the IR boundary.
• E.3 — Seller-payment vertical slice
  • julc verify dsl-init and julc verify dsl.
  • Exact-UPLC seller-paid-at-least property with a kernel-checked ledger-domain bridge.
  • Authorized, unpaid, vacuous, and deliberately multi-satisfaction-vulnerable controls.
  • Hash-bound property IR, generated Lean, artifact, dependencies, bounds, and certificate.

PR: #86

Required before E.1–E.3 are considered landed

• Refresh E.3 on top of compiler-owned strict-data-v1 boundaries.
• Remove obsolete handwritten datum tag/arity checks from the E.3 fixtures.
• Regenerate and rerun all four E.3 classifications.
• Run affected Gradle suites and zero-UPLC-effect regression tests after the main integration.
• Keep the trusted-source worker warning visible in CLI and documentation.

Pending DSL milestones

E.4 — Purpose and surface expansion

• E.4a — Minting DSL
  • Minting metamodel root and purpose-specific context.
  • Own-policy selection, minted value, token names, quantities, and signer operations.
  • Semantic equivalence target against the existing controlled-mint profile where applicable.
  • Positive, vulnerable, malformed, vacuous, and exact-artifact evidence.
• E.4b — Rewarding/withdrawal DSL
  • Withdrawal credential and amount access.
  • Reviewed ledger-domain bridge and certificate fixtures.
• E.4c — Certifying/publish DSL
  • Certificate variant and purpose/index access with exhaustive typed mapping.
• E.4d — Voting and proposing exploration
  • Blocked for normal CIP-57 artifact selection until a truthful standard purpose vocabulary or explicitly reviewed extension strategy exists.
• Expand typed spending surface: inputs, reference inputs, continuing outputs, datum witnesses, redeemers, values, fees, validity fields, and reviewed collection operations.
• Make assumptions first-class, allow-listed IR rather than arbitrary user premises.
• Decide structural versus extensional semantics for map/value equality.
• Add global multi-input/output linkage before promoting seller payment into a stable profile.

Property authoring and isolation

• Generalize beyond the fixed E.3 seller-payment AST only through reviewed IR node families.
• Improve contract-specific generated model ergonomics and diagnostics.
• Design OS-level isolation or a networkless Docker worker before hosted execution of untrusted property builders.
• Preserve deterministic IR, generated Lean, and certificate hashes across supported platforms.

E.5 — State-machine experiment

• Define a deliberately small state-machine vocabulary.
• Evaluate bounded model checking and k-induction separately.
• Keep bounded reachability, inductive evidence, and exact-validator one-step properties distinct in certificates.
• Review counterexample quality and solver scalability.

E.6 — Public API decision

• Decide whether the DSL provides enough value and stability to become public.
• Freeze names/versioning only after multi-purpose evidence exists.
• Document the trusted property-builder boundary.
• If criteria are not met, retain the DSL as experimental and keep annotations/profiles as the supported product surface.

Non-negotiable acceptance rules

• No raw Lean, axioms, sorry, admit, unsafe, partial, or unpinned imports from DSL input.
• Property declarations must not alter validator UPLC.
• Every result remains scoped to an exact artifact, named property, assumptions, model revision, and recorded bounds.
• Unsupported, unknown, timed-out, vacuous, tampered, or under-fueled work is never success.
• Typed model coverage must not be advertised as universal automated proof or whole-contract safety.

References: ADR-016 in PR #86; ADR-014; ADR-015; ADR-017.