Stuck on proving a theorem about a simple program

Stream: Program verification

[William Harvey]

Hi all! :wave: I'm new here. I'm pretty new to formal verification and lean, and I'm really trying to make an effort to lean how to formally verify simple programs. After trying to prove a theorem about one of the clever popcount implementations that you can find in the C++ Folly library (and other places), and trying out a bunch of different tools to get the job done (Ada/SPARK, Viper, Nagini, Agda, etc.), I finally decided to take a crack at it using Lean4. I got about as far as I did with the other systems, which is to say I got stuck :joy: But I've learned a lot along the way.

So I've scaled back my ambitions a bit, and instead of trying to prove correctness of popcount, I've written a tiny simple function getBits that returns the least significant bits of binary representation of an input UInt64 number. You can supply the number of bits that you want to receive as an argument. I figure, if I can prove _something_ interesting about this program, I might be able to get some momentum with proving other things about other programs.

But despite my efforts, I'm stuck on this one too. There's really great documentation out there for lean4, but it's hard to find anything substantial about program verification. The way I'm going about it may be laughably wrong. I'd really appreciate some guidance.

Here's the function and a couple #eval statements to spot check the output:

/-
 - Returns the `numBits` least significant bits of `x`
 -/
def getBits (numBits : Nat) (x : UInt64) : List Bool :=
  let rec helper (depth : Nat) (bits : List Bool) (x : UInt64) : List Bool :=
    match depth with
    | Nat.zero => bits
    | Nat.succ d2 =>
      let bit := x.mod 2 == 1
      let residual := x.shiftRight 1
      helper d2 (bits.concat bit) residual
  helper numBits [] x

#eval getBits 0 42  -- Prints out []
#eval getBits 3 42  -- Prints out [false, true, false]

And here's the theorem I'm trying to prove. Basically, I want to prove, "If you ask for numBits bits, then you'll get back numBits bits." I'm stuck at the sorry bit. I've tried a bunch of different things, but my flailing isn't getting me anywhere:

theorem getBitsLength : ∀ (numBits : Nat) (x : UInt64),
    numBits = (getBits numBits x).length := by
  intros numBits x
  induction numBits with
  | zero =>
    rfl
  | succ numBits ih =>
    sorry

Many thanks in advance for your help!

[Wojciech Nawrocki]

• Since you are doing induction, the thing to do in the inductive case succ is to try to get your goal into such a shape that the inductive hypothesis can be applied to it somewhere. Trying unfold getBits; unfold getBits.helper is a start. But when you do that, you'll realize that your induction hypothesis is not strong enough. It should universally quantify over more stuff. You can achieve this using induction .. generalizing .. with.
• In general, when proving something about a recursive program you wrote in dependent type theory, your proof will most likely have the same structure as the original program. In your case, you have a let rec helper, so it helps to also have a let rec helper theorem that proves some property of getBits.helper. Stating such a helper theorem may help you see the right inductive hypothesis. Here is a start:

theorem getBitsLength (numBits : Nat) (x : UInt64) : numBits = (getBits numBits x).length :=
    let rec helper (depth : Nat) (bits : List Bool) (x : UInt64) :
        (getBits.helper depth bits x).length = sorry := by
      induction depth generalizing ??? with
      sorry
    sorry

[Wojciech Nawrocki]

As to why there aren't many resources on program verification, it is true that most software verification these days is done using other systems such as Coq, F⋆, various automated provers and model checkers, etc. Afaict, so far Lean has been used mostly for pure mathematics, although this is perhaps slowly changing.

[William Harvey]

Thank you so much for your help! By golly I think we finally did it!!! :partying_face: Here's the final result:

theorem getBitsLengthHelper : ∀ (depth : Nat) (bits : List Bool) (x : UInt64),
                              (getBits.helper depth bits x).length = depth + bits.length := by
  intros depth bits x
  induction depth generalizing x bits with
  | zero =>
    simp
    rw [getBits.helper]
  | succ depth ih =>
    unfold getBits.helper
    simp [ih]
    rw [Nat.add_one]
    rw [Nat.add_succ]
    rw [← Nat.succ_add]
  done

theorem getBitsLength : ∀ (numBits : Nat) (x : UInt64),
                        (getBits numBits x).length = numBits := by
  unfold getBits
  simp [getBitsLengthHelper]
  done

All of your advice was spot-on. The thing that I was missing from my repertoire was understanding what it means to strengthen the induction hypothesis and how that corresponds to generalizing.

I was stuck for like two weeks on trying to finish this proof. I only get very small amounts of time to work on this stuff each day (if I'm lucky), so two weeks doesn't add up to a large number of hours. The good news is that I filled in a lot of knowledge gaps along the way, and I'm feeling more and more confident that I'll be able to use Lean4 for some real stuff soon.

Feels awesome to finally have this proof done. Thank you again!! :tada: