Why does the daily Nanoda check allow `Lean.trustCompiler`?

Stream: mathlib4

[James E Hanson]

The JSON configuration for the daily Nanoda check on Mathlib includes Lean.trustCompiler:

{
    "export_file_path": "mathlib_export.txt",
    "permitted_axioms": [
        "propext",
        "Classical.choice",
        "Quot.sound",
        "Lean.trustCompiler"
    ],
    "unpermitted_axiom_hard_error": false,
    "nat_extension": true,
    "string_extension": true,
    "print_success_message": true
}

Since this doesn't include Lean.ofReduceBool or Lean.ofReduceNat, it would still catch a native_decide proof, but why does Lean.trustCompiler need to be in there?

[Robin Arnez]

Also note that docs#Lean.ofReduceBool is a theorem under docs#Lean.trustCompiler:

private def auxTrue : Bool := true
private def auxFalse : Bool := false

theorem Lean.ofReduceBool' (a b : Bool) (h : Lean.reduceBool a = b) : a = b := by
  have : true = reduceBool auxTrue := rfl
  have : false = reduceBool auxFalse := rfl
  rw [auxFalse, auxTrue] at *
  subst h
  cases a <;> assumption

/-- info: 'Lean.ofReduceBool'' depends on axioms: [Lean.trustCompiler] -/
#guard_msgs in
#print axioms Lean.ofReduceBool'

[Chris Bailey]

Because Init includes Lean.reduceNat and Lean.reduceBool, which are opaque declarations that reference Lean.trustCompiler.

[Robin Arnez]

I mean I guess Nanoda as an external checker doesn't support compiler evaluation in the first place so adding Lean.trustCompiler doesn't actually do much of anything

[Robin Arnez]

To Nanoda, Lean.trustCompiler is just a axiom that asserts that True is true

[James E Hanson]

Sure, I understand that it's not really an issue. I just want to understand on a technical level why it was necessary.

[James E Hanson]

Chris Bailey said:

Because Init includes Lean.reduceNat and Lean.reduceBool, which are opaque declarations that reference Lean.trustCompiler.

Ah I see, so the difference is that nothing in Mathlib actually references Lean.ofReduceNat or Lean.ofReduceBool.

[Eric Wieser]

Does anything in mathlib reference trustCompiler?

[Eric Wieser]

Robin Arnez said:

Also note that docs#Lean.ofReduceBool is a theorem under docs#Lean.trustCompiler:

Why do we even have it as an axiom then?

[James E Hanson]

Eric Wieser said:

Why do we even have it as an axiom then?

This is probably a byproduct of the way these axioms were implemented. Originally there were only Lean.ofReduceNat and Lean.ofReduceBool, but there were still ways of proving things with native_decide without Lean noticing.

[James E Hanson]

Eric Wieser said:

Does anything in mathlib reference trustCompiler?

Anyway, the point is that yes, as Chris said, there are two definitions in (the imports of) Mathlib that reference trustCompiler, which are reduceBool and reduceNat:

opaque reduceBool (b : Bool) : Bool :=
  -- This ensures that `#print axioms` will track use of `reduceBool`.
  have := trustCompiler
  b

opaque reduceNat (n : Nat) : Nat :=
  -- This ensures that `#print axioms` will track use of `reduceNat`.
  have := trustCompiler
  n

Even though these are opaque, their definitions are still checked by typechecking.