[RSoulatIOHK]

Nash's sampled tests cannot express universal claims about compiled programs. Add private proof blocks and nash proof (alias verify) to check the generated UPLC with Lean-blaster, PlutusCoreBlaster and CardanoLedgerApiBlaster.

Implementation

• Accept closed test declarations and symbolic prop declarations in module-local proof blocks. Proof imports have their own scope, and production builds exclude proof bodies and imports.
• Use dedicated source and canonical Proof types, symbolic-domain binders, and execution/partial-correctness obligations. Shared parser and formatter helpers preserve the existing declaration syntax. Diagnostics reject proof budgets, invalid domains, and unsupported partial-correctness modifiers.
• Compile proof bodies through Nash's ordinary UPLC pipeline. Domains include arbitrary mathematical integers, Booleans, bytes, strings, Data, and ledger-valid V1/V2/V3 spending and minting contexts.
• Export portable Lake projects with pinned dependencies, embedded Flat bytecode, and structured metadata. Preserve each run's Lean sources, results and diagnostics. Support export without Lean and execution against an existing built Lean project.

Fuel is an execution limit: script errors and exhaustion are rejection. Passing properties require successful execution for every input; fail requires universal rejection and fail once requires a rejection witness. Solver unknowns, timeouts, crashes and malformed replies fail closed.

Proof.returns computation (\result -> condition) compiles the computation and Boolean postcondition separately. Successful returns within the computation's fuel must satisfy the condition. Computation rejection does not refute partial correctness; checker exhaustion is inconclusive. --postcondition-fuel bounds the checker independently. This does not establish termination or the existence of a successful return.

See docs/proofs.md for semantics, domains, commands and trust limits. examples/proofs provides a small runnable example.

Validation

• cargo +stable test -p nash-driver -p nash-proof: 225 passed, none failed; external-toolchain tests remain opt-in.
• cargo +stable fmt --all -- --check and diff whitespace checks pass.
• Backend regressions cover proof compilation, domain validation, import isolation, production exclusion, dedicated AST behavior, and separate computation/postcondition compilation.
• Opt-in Lean/Z3 integration regressions cover execution outcomes and exhaustion, all six supported result representations, incorrect postconditions, and checker exhaustion.

Local validation uses Rust 1.92; the repository's requested 1.98.1 toolchain is unavailable locally.

Trust and current limits

The symbolic runner reports smt_verified: results rely on the pinned libraries' models, supporting assumptions and the SMT solver. Lean kernel reconstruction is not implemented. Fuel counts CEK steps rather than Cardano CPU/memory costs.

Generic list/product/custom ADT input domains and automatic counterexample decoding/replay/shrinking are not implemented. Partial correctness supports native scalar/unit or Data-represented results. Ledger domain predicates constrain modeled contexts; they do not prove application encoding validation. Live verification requires the pinned Lean libraries and Z3.

[MicroProofs]

Oh very cool love what you are adding here

[MicroProofs]

literal casting is automatic