Heads up: changes to native_decide (and bv_decide)

Stream: lean4

[Joachim Breitner]

I’d like to quickly flag a change I’m about to merge (PR lean4#12217): As described in RFC lean4#12216, we are changing how proofs that involve native computation (native_decide, bv_decide) are represented in the proof term.

Brief summary: Instead of embedding the computation with the general ofReduceBool axiom, and the kernel then calling back to the compiler to evaluate the computation, now the tactic will run the computation and, if it returns true, assert that result using axiom : … = true. The whole ofReduceBool and Lean.trustCompiler machinery is deprecated.

The main user-impact is that if you use such tactics, then #print axioms will now show different and possibly multiple axioms:

- 'bv_axiomCheck' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound]
+ 'bv_axiomCheck' depends on axioms: [propext, Classical.choice, Quot.sound, bv_axiomCheck._native.bv_decide.ax_1_5]

You can even Ctrl-click on the axiom name and jump to the tactic that added it (H'T @Robin Arnez for the suggestion)

[Kim Morrison]

@Joachim Breitner, could the generated axioms come with a doc-string, which gives a user friendly explanation of what is going on?

Something along the lines of:

The tactic bv_decide uses an external SAT solver for some problems. That SAT solver generates a certificate which bv_decide verifies. You don't need to trust the SAT solver at all, but you are trusting bv_decide's verification code. Because this expands the trusted code base outside of the Lean kernel, each proof generated by bv_decide is wrapped as a axiom.

[Eric Wieser]

Can we avoid drowning the environment in such docstrings in cases when many axioms are generated?

[Eric Wieser]

One option would be something like

/-- Docstring goes here. -/
structure BVDecideAxiom (b : Bool) where
  eq : b = true

axiom bv_axiomCheck._native.bv_decide.ax_1_5 : BVDecideAxiom (true && true)

[Joachim Breitner]

Both good ideas worth considering, thanks.

@Eric Wieser , where do you see issues with the same docstring appearing multiple times? Documentation rendering (not sure of such an auxiliary declaration should appear there)?

[Eric Wieser]

I was thinking in olean size, but maybe reuse makes that moot.

[Eric Wieser]

But I think we do want this docstring to show up _somewhere_ in doc-gen, and if we have a public decl like BVDecideAxiom to attach it to then it's perhaps easier to understand vs attaching it to the tactic directly.

[Joachim Breitner]

Well, only if the axiom shows up in the doc-gen. we don't show other auxillary declarations (…._proof) there.