How to reason about operations on fixed size integers ?

Stream: Program verification

[Alix Trieu]

Apologies if this is stupid, but I haven't managed to find the proper lemmas to reason about fixed size integers.

As an exercise to teach myself more about Lean, I'm trying to prove the correctness of the (refined) Barrett reduction algorithm that is used in recent post quantum cryptography implementations.

I have proved the correctness for an implementation on Int given some bounds on the input, and now I want to prove the correctness for an implementation on Int16 which satisfies the range constraint by definition, but I don't see how to prove its correctness.

Any advice on how to proceed?

import Mathlib

def mod_approx (α: ℚ → ℤ) (x: ℤ) (N: ℕ): ℤ := x - ↑N * (α (x/N))

notation x "mod±" y => mod_approx round x y

def mlkem_barrett_reduce (x: ℤ) :=
  x - 3329 * (((↑x * 20159) + (2 ^ 25))/ (2 ^ 26))

-- proof elided for space
lemma mlkem_barrett_reduce_correct (x: ℤ) (Hx: |x| ≤ 2 ^ 15):
  mlkem_barrett_reduce x = x mod± 3329 := by sorry

/-
https://github.com/pq-crystals/kyber/blob/main/ref/reduce.c
int16_t barrett_reduce(int16_t a) {
  int16_t t;
  const int16_t v = ((1<<26) + KYBER_Q/2)/KYBER_Q;

  t  = ((int32_t)v*a + (1<<25)) >> 26;
  t *= KYBER_Q;
  return a - t;
}
-/
def mlkem_barrett_reduce_impl (a: Int16) :=
  let t: Int32 := (a.toInt32 * (20159: Int32) + ((1: Int32) <<< 25)) >>> 26
  let t: Int16 := 3329 * t.toInt16
  a - t

lemma mlkem_barrett_reduce_impl_correct (a: Int16):
  mlkem_barrett_reduce_impl a = Int16.ofInt ((Int16.toInt a) mod± 3329) := by
  rw [← mlkem_barrett_reduce_correct (Int16.toInt a)]
  . sorry
  . sorry

[Andrés Goens]

I think omega should handle some of these, but especially the ones you have in the end are ideal for bv_decide

[Andrés Goens]

(see https://lean-lang.org/blog/2024-10-3-lean-4120/)

[Andrés Goens]

(you'll have to phrase this in terms of BitVecs, but Int32 and Int16 should be the same)

[Henrik Böving]

There is going to be native support for IntX and UIntX in bv_decide by the end of this quarter, the current nightlies already know how to reason about UIntX with bv_decide. Though one operation that's going to mess this up is the mod_approx function as bv_decide has no way to reason about it

[Alix Trieu]

Thanks for the answers, I have tried using bv_decide, but I haven't managed to understand how to transform goals in a way bv_decide can do something. For instance, how should I phrase the following statement so that it works ?

import Mathlib

example (a: Int16): |a.toInt| ≤ 2 ^ 15 := by
  rw [Int16.toInt]
  let Hmax := BitVec.isLt a.toBitVec
  simp at Hmax
  cases Int.lt_or_le a.toBitVec.toInt 0 with
  | inl Hlt =>
    rw [BitVec.toInt_neg_iff] at Hlt; simp at *
    have Hlo: 32768 ≤ a.toBitVec.toNat := by linarith
    rw [BitVec.toInt_eq_toNat_bmod, Int.bmod]
    rw [Int.emod_eq_of_lt (by omega) (by omega)]
    simp; split; linarith
    rw [abs_of_neg]; linarith; linarith
  | inr Hle =>
    rw [BitVec.toInt_pos_iff] at Hle; simp at *
    have Hlo: a.toBitVec.toNat < 32768 := by linarith
    rw [BitVec.toInt_eq_toNat_bmod, Int.bmod]
    rw [Int.emod_eq_of_lt (by omega) (by omega)]
    simp; split; rw [abs_of_nonneg]; linarith; linarith; linarith

[Vlad Tsyrklevich]

I think one thing that complicates this is that this isn't a comparison between two BitVecs, but an Int and Int and I didn't manage it to force it to be a direct comparison between BitVecs, but I did manage this:

import Mathlib
example (a: Int16): |a.toInt| ≤ 2 ^ 15 := by
  rw [abs_le, Int16.toInt, BitVec.toInt]
  omega

I'm not sure what the right solution from the BitVec API here is, maybe there should be a good way to reason about comparisons with numbers that aren't BitVecs, maybe I'm just not aware of it.

[Vlad Tsyrklevich]

To answer the question of how to phrase it, here is a trivial example:

example (a : BitVec 8) : a ≤ 255#8 := by bv_decide

There is the sharp edge that < 256 silently truncates to < 0#8. Dealing with signed ints is a bit more complicated, since BitVec thinks signedness is really just a special rule for how to convert a BitVec represented as an unsigned int to a signed int, which you can see in the if statement after the rw here:

example (a : BitVec 8) : a.toInt < 128 := by
  rw [BitVec.toInt]
  omega