[Lean] Panic-freedom tutorial example is broken

[septract]

The Lean panic-freedom example in the tutorial appears to be broken in two ways:

• Missing shoulder-angle brackets: ⌜ ... ⌝
• Uses UInt8.HaxMul_spec_bv_rw which seems to have been deleted

Here's a version which seems to work (Claude + I couldn't figure out a way to do this that used the existing lemmas):

-- Restore the missing instHaxMul and theorem from old Hax version (commit ccb89284)
namespace UInt8

instance instHaxMul : HaxMul UInt8 where
  mul x y :=
    if (BitVec.umulOverflow x.toBitVec y.toBitVec) then .fail .integerOverflow
    else pure (x * y)

theorem HaxMul_spec_bv_rw (x y: u8) :
   ¬ (BitVec.umulOverflow x.toBitVec y.toBitVec) →
   x *? y = Result.ok (x * y)
:= by simp [instHaxMul]

end UInt8

-- Our working proof using the restored theorem
theorem square_spec (value: u8) :
  ⦃ ⌜ Playground.Square._.requires (value) = pure true ⌝ ⦄
  (Playground.Square.square value)
  ⦃ ⇓ result => ⌜ Playground.Square.__1.ensures value result = pure true ⌝ ⦄
  := by
  mvcgen
  simp [Playground.Square._.requires, Playground.Square.__1.ensures, Playground.Square.square] at *
  intros
  rw [UInt8.HaxMul_spec_bv_rw]
  simp
  bv_decide

As already raised in #1632, could I suggest adding your tutorial examples to continuous integration?

[clementblaudeau]

Indeed! Thanks for the report. The bump of Lean version changed the syntax of pre/post conditions, which broke the example. I'll fix it asap. And, indeed, we should try to put that on CI

[W95Psp]

Thanks for the report!

Just a note: the tutorial examples are actually in CI already, but the job is failing (see e.g. https://github.com/cryspen/hax/actions/runs/18826038396). That CI job checks the website of hax works correctly; e.g. no broken links and no broken examples.

To check examples are working correctly, we leverage our playground. Unfortunately, running Lean is currently not working on the playground, which breaks our CI.

I will look into the playground this week to restore our CI so that we notice Lean breakages :)