Route kernel-decidable Lean verify cases through decide +kernel

docs/lean.md

@@ -48,10 +48,14 @@ classified effect set, stub signatures, Oracle law syntax, and trace assertions.
 
 `verify` blocks become Lean proof obligations:
 
-- default (`--verify-mode auto`): `example : <lhs> = <rhs> := by native_decide`
+- default (`--verify-mode auto`): `example : <lhs> = <rhs> := by decide +kernel` when the case's whole closure is known to reduce in the Lean kernel, `:= by native_decide` otherwise
 - fallback (`--verify-mode sorry`): `example : <lhs> = <rhs> := by sorry`
 - theorem stubs (`--verify-mode theorem-skeleton`): named `theorem ... := by sorry`
 
+The tactic is chosen per case, and conservatively: `decide +kernel` costs no trust (the axiom closure stays inside Lean's core three, with no `Lean.ofReduceBool`) but only works when everything the case mentions unfolds in the kernel, so a case is routed there only when the emitter can positively establish that. Anything else — a `Float` anywhere in the closure, a fn this export spelled `partial def`, a fuel wrapper's `panic!` arm, a mutual group, a case whose expected side is not a VM ground-truth literal, a case whose emitted equation is larger than the term budget — stays on `native_decide`.
+
+Two builtin families stay on `native_decide` even though they reduce in the kernel perfectly well, because their exported model can disagree with what your program computed. `Char.toCode` panics in the model on an empty string, and a Lean `panic!` returns `default` — silently, under kernel reduction — so the case can still "prove" the recorded value. `Vector.get` / `Vector.set` narrow a negative index to `0` where the runtime returns `Option.None`, which walks the model down a branch your program never took. On `native_decide` both surface as the `PANIC at …` line `aver proof --check` fails on, so you find out instead of getting a green build.
+
 `verify ... law ...` always emits expanded sample theorems from `given` domains:
 - `theorem ..._sample_n := by native_decide`
 
@@ -158,7 +162,7 @@ aver proof my_module.av --verify-mode auto -o out/
 ```
 
 That combination means:
-- regular `verify` cases become executable Lean checks via `native_decide`
+- regular `verify` cases become executable Lean checks — `decide +kernel` where the closure reduces in the kernel, `native_decide` elsewhere
 - supported `verify law` shapes get real universal proofs
 - unsupported `verify law` shapes emit the universal theorem with a `sorry` body and an inline comment, plus the per-sample + `_checked_domain` theorems as kernel-checked evidence
 - recursive pure code inside the supported proof subset is emitted as total Lean defs

src/codegen/lean/mod.rs

@@ -7,6 +7,7 @@ mod builtins;
 mod crypto;
 mod decl_order;
 mod expr;
+mod kernel_decide;
 mod law_auto;
 pub mod lemma_calc;
 mod pattern;

src/codegen/lean/toplevel/mod.rs

@@ -22,8 +22,8 @@ pub use verify::{emit_decision, emit_verify_block};
 // paths keep resolving exactly as they did when this was a single file.
 pub(super) use super::{
     LAW_CLASS_BOUNDED_DOMAIN, LAW_CLASS_MARKER_PREFIX, LAW_CLASS_UNIVERSAL, VerifyEmitMode,
-    bound_expr_to_lean, expr, law_auto, recurrence, sample_literal, sizeof_measure_param_indices,
-    syntax, types,
+    bound_expr_to_lean, expr, kernel_decide, law_auto, recurrence, sample_literal,
+    sizeof_measure_param_indices, syntax, types,
 };
 
 /// Check if a sum type is self-referencing (any variant field mentions the type name).

src/codegen/lean/toplevel/verify.rs

@@ -1,5 +1,6 @@
 use super::VerifyEmitMode;
 use super::expr::{aver_name_to_lean, emit_expr_legacy};
+use super::kernel_decide::CaseDecidability;
 use super::law_auto::{emit_verify_law_forall_auto_proof, emit_verify_law_support_theorems};
 use super::types::type_annotation_to_lean;
 use crate::ast::*;
@@ -110,13 +111,16 @@ fn emit_sample_guard_resolved(
 
 /// Emit verify blocks as Lean 4 `example` declarations.
 ///
-/// `native_decide` gives executable proof checks for decidable goals.
-/// `sorry` is available as explicit fallback mode.
+/// A sampled case is a ground equation, so it is closed by evaluation;
+/// `decidability` picks the evaluator PER CASE — `decide +kernel` when the
+/// case's emitted closure provably reduces in the kernel, `native_decide`
+/// otherwise. `sorry` is available as explicit fallback mode.
 pub fn emit_verify_block(
     vb: &VerifyBlock,
     ctx: &CodegenContext,
     verify_mode: VerifyEmitMode,
     case_index_start: usize,
+    decidability: &CaseDecidability,
 ) -> (String, usize) {
     if let VerifyKind::Law(law) = &vb.kind {
         return emit_verify_law_block(vb, law, ctx, verify_mode, case_index_start);
@@ -145,13 +149,16 @@ pub fn emit_verify_block(
         // without an entry (verify failed/skipped, Float-carrying value —
         // decimal repr isn't bit-exact — or a shape that doesn't round-trip)
         // keep the source RHS and rely on the `--check` panic gate.
-        let right_str = super::sample_literal::ground_truth_rhs(vb, ctx, case_index_start + idx)
-            .unwrap_or_else(|| emit_expr_legacy(right, ctx, None));
+        let ground_truth = super::sample_literal::ground_truth_rhs(vb, ctx, case_index_start + idx);
+        let has_ground_truth = ground_truth.is_some();
+        let right_str = ground_truth.unwrap_or_else(|| emit_expr_legacy(right, ctx, None));
         match verify_mode {
             VerifyEmitMode::NativeDecide => {
                 lines.push(format!(
-                    "example : {} = {} := by native_decide",
-                    left_str, right_str
+                    "example : {} = {} := by {}",
+                    left_str,
+                    right_str,
+                    decidability.tactic_for(left, &left_str, &right_str, has_ground_truth, ctx)
                 ));
             }
             VerifyEmitMode::Sorry => {

src/codegen/lean/transpile.rs

@@ -221,13 +221,85 @@ fn is_wrapper_over_recursion_inner(ctx: &CodegenContext, fd: &crate::ast::FnDef)
     })
 }
 
+/// Tokens that make an emitted declaration unreducible in the kernel: a
+/// `partial def` / `opaque` / `unsafe` constant has no definitional unfolding,
+/// and a `sorry` is not a value at all.
+///
+/// A `panic!` arm (the fuel wrappers' exhaustion case) is listed for a
+/// different reason: it DOES reduce — silently, to `default` — where native
+/// evaluation prints the `PANIC at …` line that `aver proof --check` charges
+/// as a hard failure. Kernel-deciding such a case would blind that gate.
+const KERNEL_OPAQUE_TOKENS: [&str; 5] = ["partial def", "opaque ", "unsafe ", "sorry", "panic!"];
+
+/// `true` iff the kernel cannot see through what the emitter just wrote for
+/// this component.
+///
+/// Reads the fact off the emitted TEXT rather than re-deriving it from the
+/// source shape, so a new emission strategy cannot silently widen the
+/// kernel-decided set. Mutual groups are rejected wholesale: whether fuelized
+/// or well-founded, their compiled recursor is not something to bet a user's
+/// `lake build` on.
+fn component_is_kernel_opaque(comp: &[&crate::ast::FnDef], emitted: &[String]) -> bool {
+    comp.len() > 1
+        || emitted
+            .iter()
+            .any(|code| code_has_kernel_opaque_token(code))
+}
+
+/// Token scan over emitted Lean, ignoring `/-- … -/` doc comments and `--`
+/// lines. The doc text is user prose lifted from the Aver `?` description, so
+/// scanning it would classify a fn whose description merely says "opaque" as
+/// kernel-opaque. Code lines are matched with a plain `contains`: a false hit
+/// (the word inside a Lean string literal) only routes the case back to
+/// `native_decide`, which is always safe.
+fn code_has_kernel_opaque_token(code: &str) -> bool {
+    let mut in_doc = false;
+    for raw in code.lines() {
+        let line = raw.trim_start();
+        if in_doc {
+            in_doc = !line.contains("-/");
+            continue;
+        }
+        if line.starts_with("/-") {
+            in_doc = !line.contains("-/");
+            continue;
+        }
+        if line.starts_with("--") {
+            continue;
+        }
+        if KERNEL_OPAQUE_TOKENS.iter().any(|tok| line.contains(tok)) {
+            return true;
+        }
+    }
+    false
+}
+
 fn emit_pure_component(
     comp: &[&crate::ast::FnDef],
     scope: Option<&str>,
     ctx: &CodegenContext,
     emit_mode: LeanEmitMode,
     recursive_names: &HashSet<String>,
     recursive_fns: &HashSet<String>,
+    opaque_fns: &mut HashSet<crate::ir::FnId>,
+) -> Vec<String> {
+    let out = emit_pure_component_code(comp, scope, ctx, emit_mode, recursive_names, recursive_fns);
+    if component_is_kernel_opaque(comp, &out) {
+        opaque_fns.extend(
+            comp.iter()
+                .filter_map(|fd| crate::codegen::common::fn_id_for_decl(ctx, fd)),
+        );
+    }
+    out
+}
+
+fn emit_pure_component_code(
+    comp: &[&crate::ast::FnDef],
+    scope: Option<&str>,
+    ctx: &CodegenContext,
+    emit_mode: LeanEmitMode,
+    recursive_names: &HashSet<String>,
+    recursive_fns: &HashSet<String>,
 ) -> Vec<String> {
     ctx.with_module_scope(scope, || {
         let mut out = Vec::new();
@@ -394,25 +466,12 @@ pub(super) fn transpile_unified(
         }
     }
 
-    let mut entry_verify_sections: Vec<String> = Vec::new();
-    let mut verify_case_counters: HashMap<String, usize> = HashMap::new();
-    // Certificate model modules omit the `verify` sample-check `example`
-    // blocks: they are decided by `native_decide`, need the recursive-type
-    // `DecidableEq` shim the cert mode also drops, and a certificate carries
-    // its own decode-to-Int/bytes anti-vacuity guards instead.
-    if !cert_model {
-        for item in &ctx.items {
-            if let TopLevel::Verify(vb) = item {
-                let key = verify_counter_key(vb);
-                let start_idx = *verify_case_counters.get(&key).unwrap_or(&0);
-                let (emitted, next_idx) =
-                    toplevel::emit_verify_block(vb, ctx, verify_mode, start_idx);
-                verify_case_counters.insert(key, next_idx);
-                entry_verify_sections.push(emitted);
-                entry_verify_sections.push(String::new());
-            }
-        }
-    }
+    // Fns whose emission the kernel cannot see through, accumulated by every
+    // `emit_pure_component` call below. The sampled-`verify` classifier reads
+    // it AFTER both declaration passes have run — which is why the entry
+    // verify blocks are emitted at the end of this fn rather than here (their
+    // position in the output is unchanged).
+    let mut opaque_fns: HashSet<crate::ir::FnId> = HashSet::new();
 
     // ---- Per-module file bodies ----
     let mut module_files: Vec<(String, String)> = Vec::new();
@@ -463,6 +522,7 @@ pub(super) fn transpile_unified(
                         emit_mode,
                         &recursive_names,
                         &recursive_fns,
+                        &mut opaque_fns,
                     ));
                 }
             }
@@ -528,8 +588,16 @@ pub(super) fn transpile_unified(
                     }
                     let key = verify_counter_key(vb);
                     let start_idx = *dep_verify_counters.get(&key).unwrap_or(&0);
-                    let (emitted, next_idx) =
-                        toplevel::emit_verify_block(vb, ctx, verify_mode, start_idx);
+                    // Law blocks only (the `continue` above filters the rest),
+                    // and a law's proof never routes through the sampled-case
+                    // classifier — so no classification is available or needed.
+                    let (emitted, next_idx) = toplevel::emit_verify_block(
+                        vb,
+                        ctx,
+                        verify_mode,
+                        start_idx,
+                        &super::kernel_decide::CaseDecidability::disabled(),
+                    );
                     dep_verify_counters.insert(key, next_idx);
                     body_sections.push(emitted);
                     body_sections.push(String::new());
@@ -603,10 +671,48 @@ pub(super) fn transpile_unified(
                     emit_mode,
                     &recursive_names,
                     &recursive_fns,
+                    &mut opaque_fns,
                 ));
             }
         }
     }
+
+    // ---- Sampled `verify` cases (entry only) ----
+    // Emitted last so the per-case kernel-decidability classifier can read the
+    // opacity of every declaration this transpile actually produced. Only
+    // proof mode is classified: the standard emit spells every recursive fn
+    // `partial`, which no kernel reduction sees through anyway.
+    let case_decidability = match emit_mode {
+        LeanEmitMode::Proof => {
+            super::kernel_decide::CaseDecidability::new(opaque_fns, recursive_types.clone())
+        }
+        LeanEmitMode::Standard => super::kernel_decide::CaseDecidability::disabled(),
+    };
+    let mut entry_verify_sections: Vec<String> = Vec::new();
+    let mut verify_case_counters: HashMap<String, usize> = HashMap::new();
+    // Certificate model modules omit the `verify` sample-check `example`
+    // blocks: they are decided by `native_decide`, need the recursive-type
+    // `DecidableEq` shim the cert mode also drops, and a certificate carries
+    // its own decode-to-Int/bytes anti-vacuity guards instead.
+    if !cert_model {
+        for item in &ctx.items {
+            if let TopLevel::Verify(vb) = item {
+                let key = verify_counter_key(vb);
+                let start_idx = *verify_case_counters.get(&key).unwrap_or(&0);
+                let (emitted, next_idx) = toplevel::emit_verify_block(
+                    vb,
+                    ctx,
+                    verify_mode,
+                    start_idx,
+                    &case_decidability,
+                );
+                verify_case_counters.insert(key, next_idx);
+                entry_verify_sections.push(emitted);
+                entry_verify_sections.push(String::new());
+            }
+        }
+    }
+
     entry_body_sections.extend(entry_lifted_sections);
     entry_body_sections.extend(entry_decision_sections);
     entry_body_sections.extend(entry_verify_sections);

tests/fixtures/kernel_decide_declines.av

@@ -0,0 +1,57 @@
+module KernelDecideDeclines
+    intent =
+        "Pairs verify cases the kernel-decide classifier must decline with twins it must keep."
+    exposes [narrowedIndex, charCode, firstItem, takeNegative, scaleInt, banner]
+    effects []
+
+fn narrowedIndex() -> Bool
+    ? "Score the character the negative-index branch selects."
+    s = match Vector.get(Vector.fromList(["x"]), 0 - 1)
+        Option.None -> "B"
+        Option.Some(_) -> ""
+    Char.toCode(s) == 65
+
+fn charCode(text: String) -> Int
+    ? "Read the code point of the first character."
+    Char.toCode(text)
+
+fn firstItem(xs: List<Int>) -> Option<Int>
+    ? "Read the first element through a vector index."
+    Vector.get(Vector.fromList(xs), 0)
+
+fn takeNegative(xs: List<Int>) -> List<Int>
+    ? "Take a negative number of elements."
+    List.take(xs, 0 - 1)
+
+fn scaleInt(n: Int) -> Int
+    ? "Double an integer."
+    n * 2
+
+fn banner() -> String
+    ? "Grow a wide banner by repeated doubling."
+    a = "0123456789"
+    b = a + a
+    c = b + b
+    d = c + c
+    e = d + d
+    f = e + e
+    g = f + f
+    g + g
+
+verify narrowedIndex
+    narrowedIndex() => false
+
+verify charCode
+    charCode("A") => 65
+
+verify firstItem
+    firstItem([7, 8]) => Option.Some(7)
+
+verify takeNegative
+    takeNegative([1, 2, 3]) => []
+
+verify scaleInt
+    scaleInt(7) => 14
+
+verify banner
+    banner() => "01234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789"

tests/fixtures/kernel_decide_split.av

@@ -0,0 +1,33 @@
+module KernelDecideSplit
+    intent =
+        "Pairs kernel-reducible verify cases with Float ones the kernel cannot decide."
+    exposes [scaleInt, renderInt, truncate, halveFloat]
+    effects []
+
+fn scaleInt(n: Int) -> Int
+    ? "Double an integer."
+    n * 2
+
+fn renderInt(n: Int) -> String
+    ? "Render an integer as decimal text."
+    String.fromInt(n)
+
+fn truncate(value: Float) -> Int
+    ? "Truncate a float towards zero, returning an integer."
+    Int.fromFloat(value)
+
+fn halveFloat(value: Float) -> Float
+    ? "Halve a float."
+    value / 2.0
+
+verify scaleInt
+    scaleInt(7) => 14
+
+verify renderInt
+    renderInt(12) => "12"
+
+verify truncate
+    truncate(3.7) => 3
+
+verify halveFloat
+    halveFloat(5.0) => 2.5

tests/fixtures/large_domain_law.baseline.lean

@@ -8,7 +8,7 @@ set_option maxRecDepth 1000000
 def tripleSum (a : Int) (b : Int) (c : Int) : Int :=
   ((a + b) + c)
 
-example : tripleSum 1 2 3 = 6 := by native_decide
+example : tripleSum 1 2 3 = 6 := by decide +kernel
 
 -- verify law tripleSum.mirror (512 cases)
 -- given a: Int = 0..7