import Mathlib.Tactic

namespace BPF

def satisfiesTnum64 (x tval tmask : BitVec 64) : Prop :=
  (x &&& ~~~tmask) = tval

/-- Find smallest value above z satisfying a tnum -/
def tnumStep (tval tmask z : BitVec 64) : BitVec 64 :=
  let d := z - tval
  -- The same as (1 << fls64(d & ~tmask)) - 1
  let carry := d &&& ~~~tmask
  let carry := carry ||| (carry >>> 1)
  let carry := carry ||| (carry >>> 2)
  let carry := carry ||| (carry >>> 4)
  let carry := carry ||| (carry >>> 8)
  let carry := carry ||| (carry >>> 16)
  let carry := carry ||| (carry >>> 32)
  let inc := ((d ||| carry ||| ~~~tmask) + 1) &&& tmask
  tval ||| inc

theorem tnumStep_correct (tval tmask z : BitVec 64)
    (h_consistent : (tval &&& tmask) = 0)
    (h_lo : tval ≤ z)
    (h_hi : z < (tval ||| tmask)) :
    let r := tnumStep tval tmask z
    satisfiesTnum64 r tval tmask ∧
    tval ≤ r ∧ r ≤ (tval ||| tmask) ∧
    z < r ∧
    ∀ w, satisfiesTnum64 w tval tmask → z < w → r ≤ w := by
  unfold tnumStep satisfiesTnum64
  simp only []
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · bv_decide
  · bv_decide
  · bv_decide
  · bv_decide
  · intro w hw1 hw2; bv_decide

end BPF