feat: add Lean-blaster proof blocks and backend

.gitignore

@@ -11,3 +11,6 @@ target/
 elm/
 polarity/
 scratch/
+
+# Generated proof projects and solver transcripts
+examples/proofs/build/

.sampo/changesets/lean-blaster-proofs.md

@@ -0,0 +1,27 @@
+---
+cargo/nash-source: minor
+cargo/nash-ast: minor
+cargo/nash-parse: minor
+cargo/nash-can: minor
+cargo/nash-constrain: minor
+cargo/nash-solve: minor
+cargo/nash-nitpick: patch
+cargo/nash-report: minor
+cargo/nash-fmt: minor
+cargo/nash-codegen: minor
+cargo/nash-driver: minor
+cargo/nash-cli: minor
+cargo/nash-proof: minor
+---
+
+Add module-local proof blocks and a Lean-blaster proof command over compiled UPLC,
+with symbolic primitive and Cardano ledger domains, portable pinned Lean projects,
+structured results, explicit SMT trust, and CEK execution limits with exhaustion treated as rejection.
+
+Support partial correctness with `Proof.returns`, separate postcondition evaluation
+limits, and explicit inconclusive checker exhaustion.
+
+Represent proofs with dedicated source and canonical AST types, symbolic-domain
+binders, and distinct execution and successful-return obligations. Reject proof
+budgets during parsing and report proof-specific domain, expectation and
+postcondition errors before code generation.

SPEC.md

@@ -98,3 +98,13 @@ cargo fmt --all
 cargo clippy --all-targets --all-features -- -D warnings
 cargo insta test
 ```
+
+## Optional Lean-blaster proof backend
+
+- [x] Private proof blocks with typed symbolic primitive and ledger domains
+- [x] Compile property bodies through the standard UPLC backend
+- [x] Portable pinned Lean project export and structured result protocol
+- [x] Execution-limit rejection semantics and existential rejection witnesses
+- [ ] Generic symbolic list/product/custom ADT domains
+- [ ] Decode and replay SMT counterexamples in Nash
+- [ ] Kernel-checkable reconstructed proofs

crates/nash-ast/src/lib.rs

@@ -68,9 +68,51 @@ pub struct ViaBinder<'a> {
     pub generator: &'a Located<Expr<'a>>,
 }
 
+/// A canonical proof never carries randomized generators or measured budgets.
 #[derive(Debug)]
+pub struct Proof<'a> {
+    pub region: Region,
+    pub name: &'a Located<&'a str>,
+    pub binders: &'a [ProofBinder<'a>],
+    pub obligation: ProofObligation<'a>,
+}
+
+#[derive(Debug)]
+pub struct ProofBinder<'a> {
+    pub pattern: &'a Located<Pattern<'a>>,
+    pub domain: &'a Located<Expr<'a>>,
+}
+
+#[derive(Debug)]
+pub enum ProofObligation<'a> {
+    Execution {
+        expect: Expect,
+        body: &'a Located<Expr<'a>>,
+    },
+    /// Successful returns must satisfy this Boolean postcondition. Failure
+    /// modifiers cannot be represented on a partial-correctness obligation.
+    Returns {
+        computation: &'a Located<Expr<'a>>,
+        postcondition: &'a Located<Expr<'a>>,
+    },
+}
+
+impl<'a> ProofObligation<'a> {
+    pub fn expressions(&self) -> impl Iterator<Item = &'a Located<Expr<'a>>> {
+        let expressions = match *self {
+            Self::Execution { body, .. } => [Some(body), None],
+            Self::Returns {
+                computation,
+                postcondition,
+            } => [Some(computation), Some(postcondition)],
+        };
+        expressions.into_iter().flatten()
+    }
+}
+
 pub struct Module<'a> {
     pub tests: &'a [Test<'a>],
+    pub proofs: &'a [Proof<'a>],
     pub traits: &'a [&'a Located<Trait<'a>>],
     pub impls: &'a [&'a Located<Impl<'a>>],
     pub kind: ModuleKind,
@@ -923,3 +965,24 @@ mod record_tests {
         assert!(transparent.record_fields().is_none());
     }
 }
+
+impl std::fmt::Debug for Module<'_> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let mut debug = f.debug_struct("Module");
+        debug.field("tests", &self.tests);
+        if !self.proofs.is_empty() {
+            debug.field("proofs", &self.proofs);
+        }
+        debug.field("traits", &self.traits);
+        debug.field("impls", &self.impls);
+        debug.field("kind", &self.kind);
+        debug.field("name", &self.name);
+        debug.field("exports", &self.exports);
+        debug.field("docs", &self.docs);
+        debug.field("decls", &self.decls);
+        debug.field("unions", &self.unions);
+        debug.field("aliases", &self.aliases);
+        debug.field("binops", &self.binops);
+        debug.finish()
+    }
+}

crates/nash-can/src/environment.rs

@@ -60,6 +60,8 @@ pub struct Tables<'a> {
     pub fields: BTreeMap<nash_ast::QualifiedName<'a>, LabeledUnion<'a>>,
     /// Additional constructor visibility granted only by tests-block imports.
     pub test_fields: BTreeMap<nash_ast::QualifiedName<'a>, LabeledUnion<'a>>,
+    /// Constructor visibility granted only by proof-block imports.
+    pub proof_fields: BTreeMap<nash_ast::QualifiedName<'a>, LabeledUnion<'a>>,
     pub kinds: crate::kinds::KindEnv<'a>,
     pub traits: BTreeMap<nash_ast::QualifiedName<'a>, &'a TraitInfo<'a>>,
     pub impls: ImplTable<'a>,

crates/nash-can/src/error.rs

@@ -35,6 +35,17 @@ pub struct PossibleNames<'a> {
 
 #[derive(Clone, Debug)]
 pub enum Error<'a> {
+    ProofDomain {
+        region: Region,
+    },
+    ProofPartialExpectation {
+        region: Region,
+    },
+    DuplicateProof {
+        name: &'a str,
+        first: Region,
+        second: Region,
+    },
     DuplicateTest {
         name: &'a str,
         first: Region,

crates/nash-can/src/expression.rs

@@ -1712,8 +1712,8 @@ pub fn gather_typed_args<'a>(
     Ok((typed_args, current_type))
 }
 
-/// Only the outer test block is sequencing; nested expressions retain monadic do.
-pub(crate) fn canonicalize_test_block<'a>(
+/// Only the outer specification block is sequencing; nested expressions retain monadic do.
+pub(crate) fn canonicalize_specification_block<'a>(
     bump: &'a Bump,
     env: &Scope<'_, 'a>,
     stmts: &[&'a Located<nash_source::Stmt<'a>>],
@@ -1732,7 +1732,9 @@ pub(crate) fn canonicalize_test_block<'a>(
             stmt.region,
             free,
             warnings,
-            |env, free, warnings| canonicalize_test_block(bump, env, rest, last, free, warnings),
+            |env, free, warnings| {
+                canonicalize_specification_block(bump, env, rest, last, free, warnings)
+            },
         );
     }
     let (pattern, expr) = match stmt.value {
@@ -1748,7 +1750,8 @@ pub(crate) fn canonicalize_test_block<'a>(
         pattern::verify(bump, env.module, DuplicatePatternContext::Destruct, pattern)?;
     let inner = env.add_locals(&bindings)?;
     let mut body_free = FreeLocals::new();
-    let body = canonicalize_test_block(bump, &inner, rest, last, &mut body_free, warnings)?;
+    let body =
+        canonicalize_specification_block(bump, &inner, rest, last, &mut body_free, warnings)?;
     let outer = verify_bindings(WarningContext::Def, &bindings, body_free, warnings);
     merge_free_locals(free, outer, false);
     Ok(bump.alloc(Located::at(