diff --git a/docs/lean.md b/docs/lean.md index fd0d8c1d..0e9bf793 100644 --- a/docs/lean.md +++ b/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 : = := by native_decide` +- default (`--verify-mode auto`): `example : = := 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 : = := 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 diff --git a/src/codegen/lean/kernel_decide.rs b/src/codegen/lean/kernel_decide.rs new file mode 100644 index 00000000..cbe7a7ab --- /dev/null +++ b/src/codegen/lean/kernel_decide.rs @@ -0,0 +1,688 @@ +//! Per-case kernel-decidability classification for sampled `verify` cases. +//! +//! A sampled `verify` case emits as a ground equation (`f = `), +//! so it is closed by *evaluation*. Two evaluators are available and they buy +//! different things: +//! +//! - `native_decide` runs Lean's compiler/interpreter and asks the kernel to +//! trust the answer. It puts `Lean.ofReduceBool` into the theorem's axiom +//! closure — the proof rests on native evaluation, not on the kernel. +//! - `decide +kernel` reduces the `Decidable` instance IN the kernel, so +//! nothing beyond the kernel is trusted and the axiom closure stays inside +//! Lean's core three. (The `+kernel` variant is required: plain `decide` +//! stalls in the elaborator's `whnf` pre-check on these goals.) +//! +//! Kernel reduction only works when everything the case's term mentions can +//! actually unfold in the kernel, so this classifier routes a case to +//! `decide +kernel` only when it can positively establish that. +//! +//! CONSERVATIVE DEFAULT: anything this module does not positively recognise as +//! kernel-reducible emits `native_decide` — an unknown callee, an unresolvable +//! named type, an effectful fn, a higher-order argument, a new `Builtin` +//! variant. A wrong `native_decide` costs an axiom; a wrong `decide +kernel` +//! breaks the user's `lake build`. +//! +//! What the classifier rejects, and why: +//! +//! - **Float.** Lean ships no `DecidableEq Float`; the prelude supplies one +//! through an `@[implemented_by]` `opaque` constant the kernel can never +//! reduce. Any Float reachable through the closure — literal, signature, +//! record field, or `Float.*` / `Int.fromFloat` / `String.fromFloat` +//! builtin — disqualifies the case. +//! - **Recursive user types.** They carry the same `@[implemented_by]` +//! `opaque` `DecidableEq` shim (`emit_recursive_decidable_eq`). +//! - **Kernel-opaque emissions.** Whatever this transpile actually spelled as +//! `partial def`, `unsafe`, `opaque`, a `sorry`-floored proof, a `panic!` +//! arm (the fuel wrappers), or a `mutual` group. The fact is read off the +//! text the emitter produced — see `transpile::component_is_kernel_opaque` — +//! not re-derived from the source shape, so a new emission strategy cannot +//! silently widen the kernel path. +//! - **Cases without a VM ground-truth literal.** The expected side is then +//! the source RHS, which routes through the model too. Lean's `panic!` does +//! not abort: it returns `default`, printing `PANIC at …` under native +//! evaluation (which `aver proof --check` charges as a hard failure) but +//! reducing SILENTLY in the kernel. Requiring the literal keeps the equation +//! pinned to the value the program actually computed, so a defaulted model +//! cannot satisfy it and the anti-vacuity gate stays meaningful. +//! - **Builtins whose lowering can panic, or can narrow past the VM.** The +//! literal alone does NOT close the vacuity hole above: a defaulted model +//! satisfies the equation whenever `default` happens to equal the value the +//! VM computed. That is not exotic — `Bool`'s default is `false`, and half +//! of all predicate cases expect `false`. So the second half of the gate is +//! per-builtin: a lowering that can reach `panic!` on an input a program +//! can supply is not kernel-eligible. Neither is one that NARROWS an +//! argument the VM rejected into one it accepts (`Int.toNat` maps every +//! negative index to `0`), because the model then evaluates a branch the VM +//! never took — and from that branch any other builtin's `panic!` is back +//! in play, defaulted and silent. See [`builtin_panic_capability`] for the +//! audit of every entry against the prelude definition it reaches. +//! +//! - **Oversized cases.** Kernel reduction is real work and, unlike the +//! elaborator, it has no heartbeat limit to stop it — see +//! [`KERNEL_DECIDE_TERM_BUDGET`]. +//! +//! The remaining question is per-builtin, and two tables answer it: does the +//! lowering REDUCE in the kernel ([`builtin_reduces_in_kernel`], pinned +//! empirically against Lean 4.32), and is the reduction FAITHFUL to what the +//! VM computed ([`builtin_panic_capability`], audited against the prelude). +//! Both are exhaustive matches, so a new `Builtin` variant must be classified +//! on both axes before it compiles. + +use std::collections::HashSet; + +use crate::ast::{Literal, Spanned, Type, TypeDef}; +use crate::codegen::CodegenContext; +use crate::codegen::builtins::{Builtin, recognize_builtin}; +use crate::ir::hir::{ + BuiltinIntrinsic, ResolvedCallee, ResolvedCtor, ResolvedExpr, ResolvedPattern, ResolvedStmt, + ResolvedStrPart, +}; +use crate::ir::{FnId, TypeId}; + +/// Kernel-checked evaluation: no `Lean.ofReduceBool` in the axiom closure. +pub(super) const KERNEL_DECIDE_TACTIC: &str = "decide +kernel"; +/// Native evaluation: fast, but the theorem trusts the compiler. +pub(super) const NATIVE_DECIDE_TACTIC: &str = "native_decide"; + +/// Data-size budget, in characters of the emitted EQUATION — both sides — +/// above which a case keeps `native_decide` no matter how kernel-reducible it +/// is. +/// +/// Kernel reduction is not heartbeat-limited — an oversized case does not +/// error out, it just makes `lake build` slow — so the only bound available at +/// emit time is the size of the literal data the term carries. Both sides +/// count: the expected side is the VM ground-truth literal, and the kernel +/// must reduce the `Decidable` instance for the WHOLE equation, so a +/// three-token call returning a four-kilobyte list is exactly as much work as +/// the four-kilobyte argument that produced it. Budgeting the left side alone +/// let that shape through. +/// +/// Measured on Lean 4.32 with the most expensive shape the backend has +/// (SHA-256 over a byte-list literal, which also folds the list through the +/// `Bytes` range check and the hex encoder). Each case carries a constant +/// 75-character expected side (`Except.ok "<64 hex chars>"`), so as full +/// equations the measured points read: +/// +/// ```text +/// 332 chars (56-byte FIPS vector) 3.1 s +/// 661 chars (128 bytes) 5.5 s +/// 1252 chars (256 bytes) 9.0 s +/// 2422 chars (512 bytes) 21.3 s +/// ``` +/// +/// 1 KiB admits the 128-byte shape at 5.5 s and declines everything past it, +/// while still leaving three times the headroom the FIPS vectors need. +/// Cheaper shapes (plain Int / List cases) pay far less per character, so the +/// budget rejects some of them needlessly — which costs nothing but a missed +/// opportunity, the same trade every other decline in this module makes. +const KERNEL_DECIDE_TERM_BUDGET: usize = 1024; + +/// Per-transpile classifier for sampled `verify` cases. +pub(super) struct CaseDecidability { + /// Fns whose Lean emission in THIS transpile the kernel cannot see + /// through (`partial def`, fuel `panic!`, `mutual`, `sorry`, `unsafe`). + opaque_fns: HashSet, + /// Recursive user type names — they carry the `opaque` `DecidableEq` shim. + opaque_eq_types: HashSet, + /// `false` turns every case back to `native_decide`. + enabled: bool, +} + +impl CaseDecidability { + pub(super) fn new(opaque_fns: HashSet, opaque_eq_types: HashSet) -> Self { + Self { + opaque_fns, + opaque_eq_types, + enabled: true, + } + } + + /// Classification off — every case emits `native_decide`. + pub(super) fn disabled() -> Self { + Self { + opaque_fns: HashSet::new(), + opaque_eq_types: HashSet::new(), + enabled: false, + } + } + + /// Tactic for one sampled case. + /// + /// `lhs` is the case's left side (the side that routes through the model) + /// and `emitted_lhs` / `emitted_rhs` are the Lean texts the emitter + /// produced for the two sides. `ground_truth_expected` says the emitted + /// right side is the literal the VM computed rather than the source RHS — + /// required, see the module docs. The literal itself needs no walk: it is + /// pure data of the left side's type, which the walk already proves + /// kernel-safe. It does count against the budget, though — the kernel + /// reduces the equation, not the left side. + pub(super) fn tactic_for( + &self, + lhs: &Spanned, + emitted_lhs: &str, + emitted_rhs: &str, + ground_truth_expected: bool, + ctx: &CodegenContext, + ) -> &'static str { + if self.enabled + && ground_truth_expected + && emitted_lhs.len() + emitted_rhs.len() <= KERNEL_DECIDE_TERM_BUDGET + && self.closure_is_kernel_decidable(lhs, ctx) + { + KERNEL_DECIDE_TACTIC + } else { + NATIVE_DECIDE_TACTIC + } + } + + fn closure_is_kernel_decidable( + &self, + lhs: &Spanned, + ctx: &CodegenContext, + ) -> bool { + let scope = ctx.active_module_scope(); + let resolved = ctx.resolve_expr(lhs, scope.as_deref()); + let mut walk = Walk { + opaque_fns: &self.opaque_fns, + opaque_eq_types: &self.opaque_eq_types, + ctx, + seen_fns: HashSet::new(), + seen_types: HashSet::new(), + pending: Vec::new(), + }; + if !walk.expr(&resolved) { + return false; + } + while let Some(fn_id) = walk.pending.pop() { + if !walk.fn_def(fn_id) { + return false; + } + } + true + } +} + +struct Walk<'a> { + opaque_fns: &'a HashSet, + opaque_eq_types: &'a HashSet, + ctx: &'a CodegenContext, + seen_fns: HashSet, + seen_types: HashSet, + pending: Vec, +} + +impl Walk<'_> { + /// One callee's signature plus its whole body. + fn fn_def(&mut self, fn_id: FnId) -> bool { + if !self.seen_fns.insert(fn_id) { + return true; + } + if self.opaque_fns.contains(&fn_id) { + return false; + } + let Some(rfd) = self.ctx.resolved_program.fn_by_id(fn_id) else { + // Synthetic / un-indexed fn: no body to inspect. + return false; + }; + // Effectful fns emit through the Oracle lifting path (extra oracle + // params, stub injection). Out of scope for kernel classification. + if !rfd.effects.is_empty() { + return false; + } + if !self.type_is_kernel_safe(&rfd.return_type) { + return false; + } + for (_, ty) in &rfd.params { + if !self.type_is_kernel_safe(ty) { + return false; + } + } + // `rfd` borrows `self.ctx`; the body is behind an `Arc`, so clone the + // handle and drop the borrow before recursing with `&mut self`. + let body = rfd.body.clone(); + for stmt in body.stmts() { + let ok = match stmt { + ResolvedStmt::Expr(e) => self.expr(e), + ResolvedStmt::Binding { ty_ann, value, .. } => { + ty_ann + .as_ref() + .is_none_or(|ty| self.type_is_kernel_safe(ty)) + && self.expr(value) + } + }; + if !ok { + return false; + } + } + true + } + + fn exprs(&mut self, items: &[Spanned]) -> bool { + items.iter().all(|e| self.expr(e)) + } + + fn expr(&mut self, expr: &Spanned) -> bool { + match &expr.node { + ResolvedExpr::Literal(lit) => !matches!(lit, Literal::Float(_)), + // A local slot's value came from a param, a binding, or a pattern + // binder — each already visited by this walk. + ResolvedExpr::Resolved { .. } => true, + // A name the resolver left unclassified (top-level binding, fn + // value). Nothing to unfold from here. + ResolvedExpr::Ident(_) => false, + ResolvedExpr::Attr(obj, _) => self.expr(obj), + ResolvedExpr::Neg(inner) | ResolvedExpr::ErrorProp(inner) => self.expr(inner), + ResolvedExpr::BinOp(_, l, r) => self.expr(l) && self.expr(r), + ResolvedExpr::List(items) + | ResolvedExpr::Tuple(items) + | ResolvedExpr::IndependentProduct(items, _) => self.exprs(items), + ResolvedExpr::MapLiteral(entries) => { + entries.iter().all(|(k, v)| self.expr(k) && self.expr(v)) + } + ResolvedExpr::InterpolatedStr(parts) => parts.iter().all(|part| match part { + ResolvedStrPart::Literal(_) => true, + ResolvedStrPart::Parsed(e) => self.expr(e), + }), + ResolvedExpr::Match { subject, arms } => { + self.expr(subject) + && arms + .iter() + .all(|arm| self.pattern(&arm.pattern) && self.expr(&arm.body)) + } + ResolvedExpr::Ctor(ctor, args) => self.ctor(ctor) && self.exprs(args), + ResolvedExpr::RecordCreate { + type_id, + type_name, + fields, + } => { + self.named_type_is_kernel_safe(*type_id, type_name) + && fields.iter().all(|(_, e)| self.expr(e)) + } + ResolvedExpr::RecordUpdate { + type_id, + type_name, + base, + updates, + } => { + self.named_type_is_kernel_safe(*type_id, type_name) + && self.expr(base) + && updates.iter().all(|(_, e)| self.expr(e)) + } + ResolvedExpr::TailCall { target, args } => { + self.enqueue(*target); + self.exprs(args) + } + ResolvedExpr::Call(callee, args) => self.callee(callee) && self.exprs(args), + } + } + + fn callee(&mut self, callee: &ResolvedCallee) -> bool { + match callee { + ResolvedCallee::Fn(id) => { + self.enqueue(*id); + true + } + ResolvedCallee::Builtin(name) => { + recognize_builtin(name).is_some_and(builtin_is_kernel_eligible) + } + // Total Euclidean `Int` division / modulo — the literal-divisor + // discharge. Lean's `Int` division reduces in the kernel. + ResolvedCallee::Intrinsic(intrinsic) => matches!( + intrinsic, + BuiltinIntrinsic::IntDivEuclid | BuiltinIntrinsic::IntModEuclid + ), + // Higher-order fn value / resolver give-up. + ResolvedCallee::LocalSlot { .. } | ResolvedCallee::Unresolved { .. } => false, + } + } + + fn ctor(&mut self, ctor: &ResolvedCtor) -> bool { + match ctor { + ResolvedCtor::Builtin(_) => true, + ResolvedCtor::User { type_id, name, .. } => { + self.named_type_is_kernel_safe(Some(*type_id), name) + } + ResolvedCtor::Unresolved { .. } => false, + } + } + + fn pattern(&mut self, pattern: &ResolvedPattern) -> bool { + match pattern { + ResolvedPattern::Wildcard + | ResolvedPattern::Ident(_) + | ResolvedPattern::EmptyList + | ResolvedPattern::Cons(_, _) => true, + ResolvedPattern::Literal(lit) => !matches!(lit, Literal::Float(_)), + ResolvedPattern::Tuple(items) => items.iter().all(|p| self.pattern(p)), + ResolvedPattern::Ctor(ctor, _) => self.ctor(ctor), + } + } + + fn enqueue(&mut self, fn_id: FnId) { + if !self.seen_fns.contains(&fn_id) { + self.pending.push(fn_id); + } + } + + /// `true` iff no Float and no `opaque`-`DecidableEq` type can reach the + /// emitted term through this type. + fn type_is_kernel_safe(&mut self, ty: &Type) -> bool { + match ty { + Type::Int | Type::Str | Type::Bool | Type::Unit => true, + Type::Float => false, + Type::Option(inner) | Type::List(inner) | Type::Vector(inner) => { + self.type_is_kernel_safe(inner) + } + Type::Result(a, b) | Type::Map(a, b) => { + self.type_is_kernel_safe(a) && self.type_is_kernel_safe(b) + } + Type::Tuple(items) => items.iter().all(|item| self.type_is_kernel_safe(item)), + Type::Named { id, name } => self.named_type_is_kernel_safe(*id, name), + // Fn values, uninstantiated type vars, checker-recovery + // sentinels: nothing positively known. + Type::Fn(_, _, _) | Type::Var(_) | Type::Invalid => false, + } + } + + /// Resolve a named type to its declaration and scan its field types. An + /// unresolvable name (builtin service record, foreign type) is rejected — + /// the conservative default. + /// + /// IDENTITY: the declaration is found through the `TypeId` the + /// typechecker stamped on the reference, so two dependency modules' + /// same-bare-name types are distinct keys here and one cannot be scanned + /// in the other's place. Only a reference the symbol table never bound + /// (`id: None` — a builtin service record, a foreign name) falls back to + /// the source-faithful name, and that fallback either resolves to a + /// declaration or declines the case. + fn named_type_is_kernel_safe(&mut self, id: Option, name: &str) -> bool { + let key = match id { + Some(type_id) => self.ctx.symbol_table.type_entry(type_id).key.canonical(), + None => name.to_string(), + }; + // The recursive-type `DecidableEq` shim is registered under the BARE + // name, because the Lean surface is flat: `recursive_type_names` + // collects `type_def_name`, and `emit_recursive_decidable_eq` emits + // against that same bare name. Asking the bare tail here is the + // conservative side of that flattening — a same-bare-name twin of a + // recursive type is rejected along with it. + let bare = key.rsplit('.').next().unwrap_or(&key); + if self.opaque_eq_types.contains(bare) { + return false; + } + if !self.seen_types.insert(key.clone()) { + // Already being scanned higher in this walk; a genuinely + // recursive type was rejected by `opaque_eq_types` above. + return true; + } + let Some(annotations) = self.field_annotations_of(id, &key) else { + return false; + }; + annotations.iter().all(|annotation| { + let ty = crate::types::parse_type_str(annotation); + self.type_is_kernel_safe(&ty) + }) + } + + /// Every field / variant-field type annotation of the declaration the + /// canonical `key` identifies, across the entry scope and every + /// dependency module. `None` when no declaration carries that key. + /// + /// A STAMPED reference matches one declaration: the one whose own + /// `type_key_for_decl` canonicalises to the same key. An UNSTAMPED one + /// has nothing but a source name to go on, so it matches by bare name and + /// unions whatever it finds — which can only widen the annotation set, + /// i.e. decline more cases. + fn field_annotations_of(&self, id: Option, key: &str) -> Option> { + let bare = key.rsplit('.').next().unwrap_or(key); + let mut found = false; + let mut annotations = Vec::new(); + let all_defs = self + .ctx + .type_defs + .iter() + .chain(self.ctx.modules.iter().flat_map(|m| m.type_defs.iter())); + for td in all_defs { + let matches = match id { + Some(_) => { + crate::codegen::common::type_key_for_decl(self.ctx, td).canonical() == key + } + None => crate::codegen::common::type_def_name(td) == bare, + }; + if !matches { + continue; + } + found = true; + match td { + TypeDef::Product { fields, .. } => { + annotations.extend(fields.iter().map(|(_, ty)| ty.clone())); + } + TypeDef::Sum { variants, .. } => { + annotations.extend(variants.iter().flat_map(|v| v.fields.iter().cloned())); + } + } + } + found.then_some(annotations) + } +} + +/// Whether a builtin may appear in a `decide +kernel` case at all: its +/// lowering must both REDUCE in the kernel and be FAITHFUL to the value the +/// VM computed. +fn builtin_is_kernel_eligible(builtin: Builtin) -> bool { + builtin_reduces_in_kernel(builtin) && builtin_panic_capability(builtin).is_kernel_safe() +} + +/// How a builtin's Lean lowering can leave the ground the VM pinned. +/// +/// The anti-vacuity gate rests on ONE assumption: the equation states the +/// value the program actually computed, so a model that gives up and returns +/// `default` cannot satisfy it. Two things break that assumption, and Lean's +/// kernel breaks both of them silently. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum PanicCapability { + /// Total in the Lean model, and it agrees with the VM across the whole + /// argument domain. + Total, + /// Reaches a panicking construct (`panic!`, `Array.get!`, `Array.set!`), + /// but only at indices the definition itself fixes — no argument a + /// program can supply moves them out of bounds. + UnreachableByConstruction, + /// Reaches `panic!` on an input a program can supply. NOT kernel-eligible: + /// Lean's `panic!` returns `default` and, under kernel reduction, does so + /// with no diagnostic at all, so the case can prove `default = ` + /// whenever the two coincide. + Reachable, + /// Narrows an argument the VM REJECTED into one it accepts, so the model + /// evaluates a branch the VM never took. NOT kernel-eligible: the values + /// then have no VM ground truth behind them, and the branch can reach + /// another builtin's `panic!` — which is how `Vector.get(v, -1)` ends up + /// defaulting `Char.toCode ""` to `0`. + NarrowsPastVm, +} + +impl PanicCapability { + fn is_kernel_safe(self) -> bool { + match self { + PanicCapability::Total | PanicCapability::UnreachableByConstruction => true, + PanicCapability::Reachable | PanicCapability::NarrowsPastVm => false, + } + } +} + +/// Audit of every builtin's Lean lowering (`lean::builtins::emit_builtin_call`) +/// against the prelude definitions it reaches (`lean::prelude`, +/// `lean::crypto_model`), for the two ways a model can drift off the VM's +/// ground truth. Exhaustive on purpose: a new `Builtin` variant is a compile +/// error here, so it cannot inherit kernel eligibility by default. +fn builtin_panic_capability(builtin: Builtin) -> PanicCapability { + use Builtin::*; + use PanicCapability::*; + match builtin { + // `Char.toCode` (prelude `LEAN_PRELUDE_CHAR_CODE`) is + // `match s.toList.head? with … | none => panic! "…: string is empty"`. + // The empty string reaches it, and the panic defaults to `0` — equal + // to the VM's answer for plenty of neighbouring inputs, and equal to + // nothing the VM ever returns here (the VM raises a RuntimeError). + CharToCode => Reachable, + + // `Vector.get` lowers to `arr[Int.toNat i]?`. `Int.toNat` maps EVERY + // negative index to `0`, so a negative index reads element 0 in the + // model while the VM (`types/vector.rs`, `idx.to_usize()` → `None`) + // returns `Option.None`. The model then walks the `Some` arm the + // program never took. + VectorGet => NarrowsPastVm, + // `Vector.set` lowers to + // `if i < arr.size then some (arr.set! (Int.toNat i) v) else none`. + // Same narrowing (the VM returns `None` for a negative index), and + // the guard does not cover it: on an EMPTY array `-1 < 0` holds, so + // the model calls `Array.set!` out of bounds and panics. + VectorSet => NarrowsPastVm, + + // `Int.toNat` again, but here the VM narrows IDENTICALLY — + // `list::clamp_count` sends every count `<= 0` to `0` — so no input + // steers the model off the VM's path. + ListTake | ListDrop => Total, + // `String.sliceAv` clamps both bounds with `if x < 0 then 0 else …`, + // and `runtime::string_slice` clamps to `[0, len]` the same way. + StringSlice => Total, + // `String.charAtAv` and `Char.fromCode` GUARD their conversions + // (`if i < 0 then none`, `if n < 0 || n > 1114111 then none`), so the + // `.toNat` is only reached where it is exact — matching the VM's + // `to_usize()` / `to_u32()` `None`s. + StringCharAt | CharFromCode => Total, + + // `AverCrypto.compress` uses `Array.get!` / `Array.set!`, but every + // index is fixed by the definition: `words` is `Array.replicate 64` + // indexed under 64, `constants` / `initial` are 64- and 8-element + // literals, and the message offsets come from `List.range + // (message.size / 64)`, which `padded` pads to a multiple of 64. The + // `Bytes` refinement carries the 0..=255 proof its `UInt8.ofNat + // byte.toNat` needs. + CryptoSha256 => UnreachableByConstruction, + + // Plain inductives and their total combinators — `Except.ok/error`, + // `some`, `Except.withDefault`, `Option.getD`, `Option.toExcept`. + ResultOk | ResultErr | OptionSome | ResultWithDefault | OptionWithDefault + | OptionToResult => Total, + + // `Int.natAbs`, `min`/`max`, the zero-guarded `Except`-returning + // `%`/`/`, and `Int.fromString` (total, `Except`-returning, over the + // total `AverDigits.parseNatChars`). + IntAbs | IntMin | IntMax | IntMod | IntDiv | IntFromString => Total, + // `AverFloat.toInt` saturates at both ends and maps NaN to `0` — + // total. (Declined by the kernel table below regardless: Float.) + IntFromFloat => Total, + + // Lean-core Float ops plus the total prelude wrappers + // (`AverFloat.pow/round/floor/ceil`, `Float.fromString`, which + // `takeWhile Char.isDigit`-guards its digit arithmetic). None panics. + // All are declined by the kernel table below regardless: Lean has no + // kernel-reducible `DecidableEq Float`. + FloatAbs | FloatSqrt | FloatPow | FloatRound | FloatFloor | FloatCeil | FloatFromInt + | FloatFromString | FloatPi | FloatMin | FloatMax | FloatSin | FloatCos | FloatAtan2 => { + Total + } + + // Lean-core string operations and the total prelude helpers + // (`String.charsAv`, `AverString.split`, `String.fromInt` over + // `AverDigits.natDigits`, `String.fromFloat`). No `panic!`, no + // unguarded narrowing. + StringLen | StringChars | StringContains | StringStartsWith | StringEndsWith + | StringTrim | StringSplit | StringJoin | StringReplace | StringToUpper | StringToLower + | StringFromInt | StringFromFloat | StringByteLength => Total, + // No prelude definition exists for these three, so nothing can panic; + // the kernel table below declines them for that same reason. + StringRepeat | StringIndexOf | StringFromBool => Total, + + BoolOr | BoolAnd | BoolNot => Total, + + // `List.head?` / `tail?` / `take` / `drop` and friends are the total + // members of Lean's list API — no `head!` / `getElem!` anywhere. + // `find?` / `any` are total too (declined below: higher-order). + ListLen | ListHead | ListTail | ListPrepend | ListConcat | ListReverse | ListContains + | ListZip | ListFind | ListAny => Total, + + // `Array.size` / `List.toArray` / `Array.toList` are total. + // `Array.mkArray` is gone in Lean 4.32, which the kernel table below + // catches; a missing constant is a build error, not a silent default. + VectorLen | VectorFromList | ListFromVector | VectorNew => Total, + + // `AverMap.*` is a total association-list API (`get` returns `Option`, + // `remove` is `filter`, `len` is `length`) — no partial accessor. + MapGet | MapSet | MapHas | MapRemove | MapKeys | MapValues | MapEntries | MapLen + | MapFromList => Total, + } +} + +/// Whether a builtin's Lean lowering reduces in the KERNEL. +/// +/// Pinned empirically against Lean 4.32: every entry was exported through +/// `aver proof --backend lean` as a concrete sample and put to a real +/// `decide +kernel` (`tests/fixtures/kernel_decide_split.av` keeps the +/// discriminating pairs as a regression). The match is exhaustive on purpose — +/// a new `Builtin` variant is a compile error here rather than a silent +/// reclassification. Reducibility is necessary but NOT sufficient: see +/// [`builtin_panic_capability`] for the faithfulness half. +fn builtin_reduces_in_kernel(builtin: Builtin) -> bool { + use Builtin::*; + match builtin { + // Result / Option — plain inductives. + ResultOk | ResultErr | OptionSome | ResultWithDefault | OptionWithDefault + | OptionToResult => true, + + // Int — literals and arithmetic have kernel GMP acceleration. + IntAbs | IntFromString | IntMin | IntMax | IntMod | IntDiv => true, + // Lowers through `AverFloat.toInt`. + IntFromFloat => false, + + // Float — `DecidableEq Float` is an `@[implemented_by]` `opaque` + // constant, and Float literals are `OfScientific` applications the + // kernel does not evaluate. No Float goal reduces. + FloatAbs | FloatSqrt | FloatPow | FloatRound | FloatFloor | FloatCeil | FloatFromInt + | FloatFromString | FloatPi | FloatMin | FloatMax | FloatSin | FloatCos | FloatAtan2 => { + false + } + + // String — prelude helpers plus Lean core operations that unfold on + // concrete strings. + StringLen | StringCharAt | StringChars | StringSlice | StringStartsWith + | StringEndsWith | StringSplit | StringJoin | StringToUpper | StringToLower + | StringFromInt | StringByteLength => true, + // Probed stuck on Lean 4.32: `containsSubstr` goes through + // `String.Slice` iteration, `trim`/`replace` through `String.Pos` + // arithmetic — the kernel does not get these to `isTrue`/`isFalse`. + StringContains | StringTrim | StringReplace => false, + // Unreachable from source today (the checker registers no signature), + // so they have never been probed. + StringRepeat | StringIndexOf => false, + // Carries a Float; and `String.fromBool` has no prelude definition at + // all (its native emission is already broken). + StringFromFloat | StringFromBool => false, + + BoolOr | BoolAnd | BoolNot => true, + + // Both reduce; `Char.toCode` is nevertheless declined, by the + // faithfulness table (its `panic!` arm). + CharToCode | CharFromCode => true, + + // The exported SHA-256 model is total and axiom-free (it folds over a + // computed block count instead of a kernel-opaque `while`), so a + // concrete digest reduces in the kernel. + CryptoSha256 => true, + + ListLen | ListHead | ListTail | ListPrepend | ListTake | ListDrop | ListConcat + | ListReverse | ListContains | ListZip => true, + // Take a fn value; the walk cannot follow a higher-order argument. + ListFind | ListAny => false, + + // All reduce; `Vector.get` / `Vector.set` are nevertheless declined, + // by the faithfulness table (their `Int.toNat` index narrowing). + VectorGet | VectorSet | VectorLen | VectorFromList | ListFromVector => true, + // Lowers to `Array.mkArray`, which Lean 4.32 no longer defines. + VectorNew => false, + + MapGet | MapSet | MapHas | MapRemove | MapKeys | MapValues | MapEntries | MapLen + | MapFromList => true, + } +} diff --git a/src/codegen/lean/mod.rs b/src/codegen/lean/mod.rs index de9519b2..89b4e7f1 100644 --- a/src/codegen/lean/mod.rs +++ b/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; diff --git a/src/codegen/lean/toplevel/mod.rs b/src/codegen/lean/toplevel/mod.rs index 4c627dd2..75c35998 100644 --- a/src/codegen/lean/toplevel/mod.rs +++ b/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). diff --git a/src/codegen/lean/toplevel/verify.rs b/src/codegen/lean/toplevel/verify.rs index aca8d68b..d636cad8 100644 --- a/src/codegen/lean/toplevel/verify.rs +++ b/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 => { diff --git a/src/codegen/lean/transpile.rs b/src/codegen/lean/transpile.rs index bfe4a8a5..4519cd62 100644 --- a/src/codegen/lean/transpile.rs +++ b/src/codegen/lean/transpile.rs @@ -221,6 +221,59 @@ 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>, @@ -228,6 +281,25 @@ fn emit_pure_component( emit_mode: LeanEmitMode, recursive_names: &HashSet, recursive_fns: &HashSet, + opaque_fns: &mut HashSet, +) -> Vec { + 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, + recursive_fns: &HashSet, ) -> Vec { 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 = Vec::new(); - let mut verify_case_counters: HashMap = 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 = 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 = Vec::new(); + let mut verify_case_counters: HashMap = 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); diff --git a/tests/fixtures/kernel_decide_declines.av b/tests/fixtures/kernel_decide_declines.av new file mode 100644 index 00000000..ed94fd1d --- /dev/null +++ b/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) -> Option + ? "Read the first element through a vector index." + Vector.get(Vector.fromList(xs), 0) + +fn takeNegative(xs: List) -> List + ? "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" diff --git a/tests/fixtures/kernel_decide_split.av b/tests/fixtures/kernel_decide_split.av new file mode 100644 index 00000000..1e3a74cb --- /dev/null +++ b/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 diff --git a/tests/fixtures/large_domain_law.baseline.lean b/tests/fixtures/large_domain_law.baseline.lean index c8f73163..72cb541c 100644 --- a/tests/fixtures/large_domain_law.baseline.lean +++ b/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 diff --git a/tests/proof_spec/lean_kernel.rs b/tests/proof_spec/lean_kernel.rs index 5af3e8a7..542b1a26 100644 --- a/tests/proof_spec/lean_kernel.rs +++ b/tests/proof_spec/lean_kernel.rs @@ -1770,3 +1770,532 @@ fn proof_lean_crypto_sha256_model_axiom_closure_is_core_only() { } let _ = std::fs::remove_dir_all(&root); } + +/// Split each `#print axioms ` block in `lake env lean` stdout into a +/// `(name, axioms)` pair. Both shapes the command emits are handled: +/// +/// ```text +/// 'foo' does not depend on any axioms +/// 'foo' depends on axioms: [propext, Quot.sound] +/// ``` +fn axiom_report_pairs(stdout: &str) -> Vec<(String, Vec)> { + let mut out = Vec::new(); + for line in stdout.lines() { + let Some(rest) = line.strip_prefix('\'') else { + continue; + }; + let Some((name, tail)) = rest.split_once('\'') else { + continue; + }; + let axioms = match tail.split_once('[') { + Some((_, listed)) => listed + .trim_end_matches(']') + .split(',') + .map(str::trim) + .filter(|a| !a.is_empty()) + .map(str::to_string) + .collect(), + None => Vec::new(), + }; + out.push((name.to_string(), axioms)); + } + out +} + +#[test] +fn proof_lean_crypto_verify_cases_are_kernel_decided_and_axiom_clean() { + // Per-case tactic routing for sampled `verify` cases. A case whose whole + // emitted closure reduces in the kernel is closed by `decide +kernel`, so + // nothing beyond the kernel is trusted. `stdlib_bytes_app` is the + // discriminating fixture: its SHA-256 and byte-range cases route through + // the total, axiom-free crypto model and the well-founded `Bytes` helpers + // (all kernel-reducible), while its hex cases route through + // `Bytes.parseHexChars`, which the proof backend emits as `partial def` — + // an opaque constant the kernel can never unfold. One file, both verdicts, + // so a classifier that collapses to "always native" or "always kernel" + // fails here. + // + // Then the real gate: `#print axioms`. `native_decide` puts + // `Lean.ofReduceBool` into a theorem's axiom closure; `decide +kernel` + // must not. Emitted `example` declarations are anonymous (Lean adds no + // name to the environment), so the probe restates each kernel-decided case + // VERBATIM as a named theorem with the emitted tactic and audits that. + // A misclassified case fails to elaborate there, which fails this test. + // + // The routing half needs no `lake`; only the build + axiom audit do. + let aver_bin = env!("CARGO_BIN_EXE_aver"); + let repo_root = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let root = temp_output_dir("aver-proof-crypto-kernel-decide"); + let missing_module_root = root.join("no-project-modules"); + let out = root.join("lean"); + let export = Command::new(aver_bin) + .current_dir(&repo_root) + .arg("proof") + .arg("tests/fixtures/stdlib_bytes_app.av") + .arg("--module-root") + .arg(&missing_module_root) + .arg("--backend") + .arg("lean") + .arg("-o") + .arg(&out) + .output() + .expect("aver proof export for the crypto kernel-decide probe"); + assert!( + export.status.success(), + "proof export failed:\n{}", + format_output(&export) + ); + let entry = std::fs::read_to_string(out.join("StdlibBytesApp.lean")) + .expect("read emitted StdlibBytesApp.lean"); + let cases: Vec<&str> = entry + .lines() + .filter(|l| l.starts_with("example : ")) + .collect(); + + for (fns, tactic, why) in [ + ( + [ + "shaHex ", + "doubleShaHex ", + "roundTrip ", + "checkedDigestLength ", + ] + .as_slice(), + "decide +kernel", + "reduces in the kernel end to end", + ), + ( + ["hexRoundTrip ", "checkedDigestHex "].as_slice(), + "native_decide", + "routes through the `partial def` hex parser", + ), + ] { + for needle in fns { + let matching: Vec<&&str> = cases.iter().filter(|l| l.contains(needle)).collect(); + assert!( + !matching.is_empty(), + "no emitted case mentions `{needle}`:\n{entry}" + ); + for line in matching { + assert!( + line.ends_with(&format!(":= by {tactic}")), + "`{needle}` {why}, so it must be closed by `{tactic}`:\n{line}" + ); + } + } + } + + if Command::new("lake").arg("--version").output().is_err() { + eprintln!("skipping crypto kernel-decide build + axiom audit: `lake` not available"); + let _ = std::fs::remove_dir_all(&root); + return; + } + let build = Command::new("lake") + .current_dir(&out) + .arg("build") + .output() + .expect("lake build for the crypto kernel-decide probe"); + assert!( + build.status.success(), + "lake build failed — a kernel-decided case did not reduce:\n{}", + format_output(&build) + ); + + let mut probe = String::from("import StdlibBytesApp\n\nset_option maxRecDepth 1000000\n\n"); + let mut probe_names = Vec::new(); + for (idx, line) in cases + .iter() + .filter(|l| l.ends_with(":= by decide +kernel")) + .enumerate() + { + let prop = line + .trim_start_matches("example : ") + .trim_end_matches(":= by decide +kernel") + .trim(); + let name = format!("averKernelCase{}", idx + 1); + probe.push_str(&format!("theorem {name} : {prop} := by decide +kernel\n")); + probe_names.push(name); + } + assert!( + probe_names.len() >= 7, + "expected the crypto fixture to contribute several kernel cases, got {}", + probe_names.len() + ); + for name in &probe_names { + probe.push_str(&format!("#print axioms {name}\n")); + } + std::fs::write(out.join("KernelAxiomProbe.lean"), probe).expect("write KernelAxiomProbe.lean"); + let audit = Command::new("lake") + .current_dir(&out) + .arg("env") + .arg("lean") + .arg("KernelAxiomProbe.lean") + .output() + .expect("lake env lean KernelAxiomProbe.lean"); + assert!( + audit.status.success(), + "kernel-decided cases failed to re-elaborate as named theorems:\n{}", + format_output(&audit) + ); + let stdout = String::from_utf8_lossy(&audit.stdout); + let reports = axiom_report_pairs(&stdout); + assert_eq!( + reports.len(), + probe_names.len(), + "expected one axiom report per kernel-decided case:\n{stdout}" + ); + for (name, axioms) in reports { + for axiom in axioms { + assert!( + matches!( + axiom.as_str(), + "propext" | "Classical.choice" | "Quot.sound" + ), + "kernel-decided case `{name}` depends on non-core axiom `{axiom}` — \ + `decide +kernel` must not pull `Lean.ofReduceBool`:\n{stdout}" + ); + } + } + let _ = std::fs::remove_dir_all(&root); +} + +#[test] +fn proof_lean_float_verify_cases_stay_native_decide() { + // Conservative half of the classifier. Lean ships no `DecidableEq Float` + // — the prelude supplies one through an `@[implemented_by]` `opaque` + // constant the kernel can never reduce — and Float literals are + // `OfScientific` applications it does not evaluate either. So no case + // whose closure touches a Float may be routed to `decide +kernel`, and + // that includes `truncate`, whose RESULT is an `Int`: the Float only + // appears in its parameter and inside `AverFloat.toInt`. + // + // The fixture pairs the Float cases with Int/String twins in ONE file, so + // the pin catches both a classifier that lets Float through and one that + // has quietly stopped classifying anything. + // + // The routing half needs no `lake`; only the build does. + let aver_bin = env!("CARGO_BIN_EXE_aver"); + let repo_root = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let out = temp_output_dir("aver-proof-kernel-decide-split"); + let export = Command::new(aver_bin) + .current_dir(&repo_root) + .arg("proof") + .arg("tests/fixtures/kernel_decide_split.av") + .arg("--backend") + .arg("lean") + .arg("-o") + .arg(&out) + .output() + .expect("aver proof export for the Float verify-tactic pin"); + assert!( + export.status.success(), + "proof export failed:\n{}", + format_output(&export) + ); + let entry = std::fs::read_to_string(out.join("KernelDecideSplit.lean")) + .expect("read emitted KernelDecideSplit.lean"); + for (needle, tactic) in [ + ("scaleInt 7", "decide +kernel"), + ("renderInt 12", "decide +kernel"), + ("truncate 3.7", "native_decide"), + ("halveFloat 5.0", "native_decide"), + ] { + let line = entry + .lines() + .find(|l| l.starts_with("example : ") && l.contains(needle)) + .unwrap_or_else(|| panic!("no emitted case for `{needle}`:\n{entry}")); + assert!( + line.ends_with(&format!(":= by {tactic}")), + "case `{needle}` must be closed by `{tactic}`:\n{line}" + ); + } + if Command::new("lake").arg("--version").output().is_err() { + eprintln!("skipping Float verify-tactic build: `lake` not available"); + let _ = std::fs::remove_dir_all(&out); + return; + } + let build = Command::new("lake") + .current_dir(&out) + .arg("build") + .output() + .expect("lake build for the Float verify-tactic pin"); + assert!( + build.status.success(), + "lake build failed:\n{}", + format_output(&build) + ); + let _ = std::fs::remove_dir_all(&out); +} + +/// Emitted `example` line whose statement contains `needle`. +fn emitted_case_line<'a>(entry: &'a str, needle: &str) -> &'a str { + entry + .lines() + .find(|l| l.starts_with("example : ") && l.contains(needle)) + .unwrap_or_else(|| panic!("no emitted case for `{needle}`:\n{entry}")) +} + +/// Export `tests/fixtures/kernel_decide_declines.av` and return the emitted +/// entry module. Shared by the two classifier-decline pins below. +fn export_kernel_decide_declines(out: &std::path::Path) -> String { + let aver_bin = env!("CARGO_BIN_EXE_aver"); + let repo_root = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let export = Command::new(aver_bin) + .current_dir(&repo_root) + .arg("proof") + .arg("tests/fixtures/kernel_decide_declines.av") + .arg("--backend") + .arg("lean") + .arg("-o") + .arg(out) + .output() + .expect("aver proof export for the kernel-decide decline pins"); + assert!( + export.status.success(), + "proof export failed:\n{}", + format_output(&export) + ); + std::fs::read_to_string(out.join("KernelDecideDeclines.lean")) + .expect("read emitted KernelDecideDeclines.lean") +} + +#[test] +fn proof_lean_panic_capable_builtins_stay_native_decide() { + // The ground-truth literal alone does NOT close the vacuity hole. Lean's + // `panic!` returns `default`, and under KERNEL reduction it does so with + // no diagnostic — so a model that panics still proves the equation + // whenever `default` equals what the VM computed. `false` is `Bool`'s + // default, which is half of all predicate cases. + // + // `narrowedIndex` is the two-step version an audit of single builtins + // misses: `Vector.get(v, -1)` lowers to `v[Int.toNat (-1)]?` = `v[0]?`, so + // the model takes the `Some` arm the VM never took (the VM returns + // `Option.None`), lands on `Char.toCode ""`, and defaults that panic to + // `0`. `0 == 65` is `false` — the very literal the VM recorded. Under + // `decide +kernel` that builds green and silent; under `native_decide` the + // `PANIC at …` line makes `aver proof --check` fail the run. + // + // So both seams are declined per-builtin: `Char.toCode` because it can + // panic on an input a program can supply, `Vector.get` because it narrows + // a negative index the VM rejected into one it accepts. The decline is + // keyed on the BUILTIN, not on the case — `charCode "A"` and + // `firstItem [7, 8]` never come near a bad index, and still route native. + // Proving in-bounds-ness per case is exactly the reasoning this + // classifier refuses to do. + // + // The twins are the other half: `List.take` narrows through the SAME + // `Int.toNat`, but the VM clamps identically (`list::clamp_count`), so it + // stays kernel-decided — the audit is per-lowering, not a retreat from + // `Int.toNat`. `scaleInt` pins that plain Int cases survive too. + // + // The routing half needs no `lake`; only the panic-gate half does. + let out = temp_output_dir("aver-proof-kernel-decide-declines"); + let entry = export_kernel_decide_declines(&out); + for (needle, tactic, why) in [ + ( + "narrowedIndex", + "native_decide", + "reaches a defaulted `Char.toCode` panic through a narrowed index", + ), + ( + "charCode \"A\"", + "native_decide", + "calls the panic-capable `Char.toCode`", + ), + ( + "firstItem [7, 8]", + "native_decide", + "calls the index-narrowing `Vector.get`", + ), + ( + "takeNegative [1, 2, 3]", + "decide +kernel", + "narrows its count exactly as the VM does", + ), + ("scaleInt 7", "decide +kernel", "is plain Int arithmetic"), + ] { + let line = emitted_case_line(&entry, needle); + assert!( + line.ends_with(&format!(":= by {tactic}")), + "case `{needle}` {why}, so it must be closed by `{tactic}`:\n{line}" + ); + } + + if Command::new("lake").arg("--version").output().is_err() { + eprintln!("skipping kernel-decide decline panic gate: `lake` not available"); + let _ = std::fs::remove_dir_all(&out); + return; + } + // The demotion has to make the panic VISIBLE, not merely move it: with + // `narrowedIndex` on `native_decide`, `aver proof --check` sees the + // `PANIC at …` line and fails the run. Under `decide +kernel` the same + // file reported `model_panicked: false, passed: true`. + let aver_bin = env!("CARGO_BIN_EXE_aver"); + let repo_root = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let checked = temp_output_dir("aver-proof-kernel-decide-declines-check"); + let run = Command::new(aver_bin) + .current_dir(&repo_root) + .arg("proof") + .arg("tests/fixtures/kernel_decide_declines.av") + .arg("--backend") + .arg("lean") + .arg("-o") + .arg(&checked) + .arg("--check") + .arg("--check-json") + .output() + .expect("aver proof --check --check-json for the panic gate"); + let json_line = String::from_utf8_lossy(&run.stdout) + .lines() + .rev() + .find(|l| l.starts_with('{')) + .map(str::to_string) + .unwrap_or_else(|| panic!("no JSON line:\n{}", format_output(&run))); + let summary: serde_json::Value = + serde_json::from_str(&json_line).unwrap_or_else(|e| panic!("bad JSON ({e}):\n{json_line}")); + assert_eq!( + ( + summary["model_panicked"].as_bool(), + summary["passed"].as_bool(), + summary["build_errors"].as_u64(), + ), + (Some(true), Some(false), Some(0)), + "the demoted case must surface its model panic as a HARD `--check` \ + failure (and the kernel-decided twins must still build):\n{}", + format_output(&run) + ); + let _ = std::fs::remove_dir_all(&out); + let _ = std::fs::remove_dir_all(&checked); +} + +#[test] +fn proof_lean_oversized_expected_literal_falls_back_to_native() { + // The term budget guards `lake build` wall-clock, and the kernel reduces + // the EQUATION — so both sides count. `banner` is the shape a left-side- + // only budget lets through: a six-character call whose ground-truth + // literal is 1280 characters of string data. The pin asserts the fallback + // AND that the left side is comfortably under budget on its own, so the + // test cannot pass for the wrong reason. + let out = temp_output_dir("aver-proof-kernel-decide-budget"); + let entry = export_kernel_decide_declines(&out); + let line = emitted_case_line(&entry, "banner = "); + let statement = line + .trim_start_matches("example : ") + .trim_end_matches(":= by native_decide") + .trim(); + let (lhs, rhs) = statement + .split_once(" = ") + .unwrap_or_else(|| panic!("expected an equation:\n{statement}")); + assert!( + lhs.len() < 64 && rhs.len() > 1024, + "the budget fixture must pair a tiny left side with an oversized \ + expected literal, got {} / {} chars", + lhs.len(), + rhs.len() + ); + assert!( + line.ends_with(":= by native_decide"), + "a case whose expected literal blows the term budget must fall back to \ + `native_decide`:\n{}", + &line[..line.len().min(120)] + ); + let _ = std::fs::remove_dir_all(&out); +} + +#[test] +fn proof_lean_kernel_decide_keys_named_types_by_stamped_identity() { + // The classifier walks a case's named types to rule out Float and the + // `opaque`-`DecidableEq` shim. Which DECLARATION a `Type::Named` refers to + // is a typed-identity question, not a string one: `Metrics.Reading` and + // `Sensors.Reading` are two records with one bare name, and only the + // second carries a Float. Keying the field scan on the bare name unions + // both declarations, so `Metrics.Reading` inherits a Float it does not + // have and every case touching it falls to `native_decide` — a silent + // loss of kernel coverage that grows with every same-named type in the + // dependency graph. The scan follows the `TypeId` the typechecker stamped + // instead, so `tally` stays kernel-decided even though a Float-carrying + // namesake is in scope. (Revert to the bare-name scan and this case emits + // `native_decide`.) + // + // Routing only — no `lake` needed. + let aver_bin = env!("CARGO_BIN_EXE_aver"); + let src = temp_output_dir("aver-kernel-decide-identity-src"); + std::fs::create_dir_all(&src).expect("create src dir"); + std::fs::write( + src.join("Metrics.av"), + "module Metrics\n\ + \x20 intent =\n\ + \x20 \"Counter readings carrying whole units only.\"\n\ + \x20 exposes [Reading, of, count]\n\ + \x20 effects []\n\n\ + record Reading\n\ + \x20 count: Int\n\n\ + fn of(n: Int) -> Reading\n\ + \x20 ? \"Wrap a whole-unit count.\"\n\ + \x20 Reading(count = n)\n\n\ + fn count(r: Reading) -> Int\n\ + \x20 ? \"Read the whole-unit count back.\"\n\ + \x20 r.count\n", + ) + .expect("write Metrics.av"); + std::fs::write( + src.join("Sensors.av"), + "module Sensors\n\ + \x20 intent =\n\ + \x20 \"Analogue readings carrying a fractional level.\"\n\ + \x20 exposes [Reading, of, tag]\n\ + \x20 effects []\n\n\ + record Reading\n\ + \x20 tag: Int\n\ + \x20 level: Float\n\n\ + fn of(n: Int) -> Reading\n\ + \x20 ? \"Wrap a tag alongside a fixed level.\"\n\ + \x20 Reading(tag = n, level = 0.5)\n\n\ + fn tag(r: Reading) -> Int\n\ + \x20 ? \"Read the tag back.\"\n\ + \x20 r.tag\n", + ) + .expect("write Sensors.av"); + std::fs::write( + src.join("Consumer.av"), + "module Consumer\n\ + \x20 intent =\n\ + \x20 \"Reads two dependency modules that both declare a type named Reading.\"\n\ + \x20 depends [Metrics, Sensors]\n\ + \x20 exposes [tally]\n\ + \x20 effects []\n\n\ + fn tally(n: Int) -> Int\n\ + \x20 ? \"Round-trip a count through the whole-unit reading.\"\n\ + \x20 Metrics.count(Metrics.of(n))\n\n\ + verify tally\n\ + \x20 tally(7) => 7\n", + ) + .expect("write Consumer.av"); + let out = temp_output_dir("aver-kernel-decide-identity-out"); + let export = Command::new(aver_bin) + .arg("proof") + .arg(src.join("Consumer.av")) + .arg("--module-root") + .arg(&src) + .arg("--backend") + .arg("lean") + .arg("-o") + .arg(&out) + .output() + .expect("aver proof export for the named-type identity pin"); + assert!( + export.status.success(), + "proof export failed:\n{}", + format_output(&export) + ); + let entry = std::fs::read_to_string(out.join("Consumer.lean")).expect("read Consumer.lean"); + let line = emitted_case_line(&entry, "tally 7"); + assert!( + line.ends_with(":= by decide +kernel"), + "`Metrics.Reading` carries only an Int, so the case must stay \ + kernel-decided — a Float-carrying `Sensors.Reading` namesake must not \ + be scanned in its place:\n{line}" + ); + let _ = std::fs::remove_dir_all(&src); + let _ = std::fs::remove_dir_all(&out); +}