How to deal with equalities over `BitVec.cast`

Stream: new members

[Ayhon]

EDIT: subst does not suffice if the equality is over expressions, not variables.

I'm running into an issue when trying to proceed with a proof over BitVecs. I try to perform a rewriting on a term which appears both in a expression and in the type of the expression, and Lean complains that the motive used for the rewriting is not type correct. I've managed to reduce the instance of this problem to the following example.

example
  (f: (n:Nat) → BitVec n)
  (res foo: Nat)
  (h: foo = res)
: f res = (f foo).cast h
:= by
  sorry

I was wondering what was the general way to deal with this. I've tried using an extensionality lemma over BitVec to remove the use of BitVec.cast with BitVec.getElem_cast and then congr to reduce the goal to res = foo but I'm left dealing with HEqs which I don't know how to handle.

My attempt so far

This is as far as I've gotten with the example, using my own BitVec.ext lemma.

import Mathlib -- for `generalize_proofs`

@[ext]
theorem BitVec.ext{bv1 bv2: BitVec n}
{point_eq: ∀ i: Nat, (_: i < n) → bv1[i] = bv2[i]}
: bv1 = bv2
:= by
  obtain ⟨⟨a, a_lt⟩⟩ := bv1
  obtain ⟨⟨b, b_lt⟩⟩ := bv2
  simp
  simp [BitVec.getElem_eq_testBit_toNat] at point_eq
  apply Nat.eq_of_testBit_eq
  intro i
  if h: i < n then
    exact point_eq i h
  else
    have: a < 2 ^i := calc
      a < 2 ^n := a_lt
      _ ≤ 2 ^i := Nat.pow_le_pow_of_le Nat.one_lt_two (Nat.le_of_not_gt h)
    simp [Nat.testBit_lt_two_pow this]
    have: b < 2 ^i := calc
      b < 2 ^n := b_lt
      _ ≤ 2 ^i := Nat.pow_le_pow_of_le Nat.one_lt_two (Nat.le_of_not_gt h)
    simp [Nat.testBit_lt_two_pow this]


example
  (f: (n:Nat) → BitVec n)
  (res foo: Nat)
  (h: foo = res)
: f (res) = (f (foo)).cast h
:= by
  ext i i_idx
  simp
  congr
  · exact h.symm
  · rw [h]
  · exact h.symm
  · exact h.symm
  · generalize_proofs i_idx_foo
    sorry

[Ayhon]

While making sure that my examples worked in the playground, I thought of using aesop to close the goal, and discovered that I could use subst h to close the goal. This doesn't translate to the original proof I had this issue over, however, since the Nat terms are not variables, but results of an expression.

I adapted my example to include an intermediate function g which prevents subst from working.

example
  (f: (n:Nat) → BitVec n)
  (g: Nat → Nat)
  (res foo: Nat)
  (h: g foo = g res)
: f (g res) = (f (g foo)).cast h
:= by sorry

This prevents aesop? from finding a proof from the start, but still allows it to finish the proof when using BitVec.ext and congr, using simp_all only [heq_eq_eq] to prove HEq a b with a: i < g res and b: i < g foo. I'm not sure what this tactic is doing though, and how it's able to close the goal.

My attempt so far

import Mathlib -- for `generalize_proofs`

@[ext]
theorem BitVec.ext{bv1 bv2: BitVec n}
{point_eq: ∀ i: Nat, (_: i < n) → bv1[i] = bv2[i]}
: bv1 = bv2
:= by
  obtain ⟨⟨a, a_lt⟩⟩ := bv1
  obtain ⟨⟨b, b_lt⟩⟩ := bv2
  simp
  simp [BitVec.getElem_eq_testBit_toNat] at point_eq
  apply Nat.eq_of_testBit_eq
  intro i
  if h: i < n then
    exact point_eq i h
  else
    have: a < 2 ^i := calc
      a < 2 ^n := a_lt
      _ ≤ 2 ^i := Nat.pow_le_pow_of_le Nat.one_lt_two (Nat.le_of_not_gt h)
    simp [Nat.testBit_lt_two_pow this]
    have: b < 2 ^i := calc
      b < 2 ^n := b_lt
      _ ≤ 2 ^i := Nat.pow_le_pow_of_le Nat.one_lt_two (Nat.le_of_not_gt h)
    simp [Nat.testBit_lt_two_pow this]


example
  (f: (n:Nat) → BitVec n)
  (g: Nat → Nat)
  (res foo: Nat)
  (h: g foo = g res)
: f (g res) = (f (g foo)).cast h
:= by
  ext i i_idx
  simp
  congr 2
  · exact h.symm
  · rw [h]
  · exact h.symm
  · exact h.symm
  · generalize_proofs i_idx_foo
    simp_all only [heq_eq_eq]

[Robin Arnez]

What about

example (f : (n : Nat) → BitVec n) (g : Nat → Nat) (res foo : Nat) (h : g foo = g res) :
    f (g res) = (f (g foo)).cast h := by
  rw [BitVec.toNat_eq]
  simp only [BitVec.toNat_cast]
  rw [h]

Or is that also not what you're really dealing with?

[Ayhon]

Translating the equality to work over Nat instead of BitVec does away with the issue. Now I'm encountering another problem where rw will perform the rewrite but simp will not, but this is a separate concern (this is a problem because I have a bunch of rewritings I'd like to do, and manually figuring out which rewritings I have to take is not what I'd like to do. I'd like to just simp [*]), so if I don't manage to figure it out on my own I'll open a new topic.

Thanks!

[Notification Bot]

Ayhon has marked this topic as resolved.

[Robin Arnez]

What about

example (f : (n : Nat) → BitVec n) (g : Nat → Nat) (res foo : Nat) (h : g foo = g res) :
    f (g res) = (f (g foo)).cast h := by
  rw [BitVec.toNat_eq]
  simp only [BitVec.toNat_cast]
  let f' := fun n => (f n).toNat
  change f' (g res) = f' (g foo)
  simp [h]

[Robin Arnez]

although I'm not sure whether that works too well with simp [*]

[Notification Bot]

Ayhon has marked this topic as unresolved.

[Ayhon]

I've been trying a bit more in the larger proof I'm working with, and it seems like my previous example does not do it enough justice. I have a bunch of equalities over BitVec n which I'm not able to rewrite, probably because of similar issues. With the toNat_eq trick I'm able to perform some of the rewrites, by removing the equality over dependent types, but I'm unable to apply other rewritings in nested expressions.

The actual usecase I'm dealing with is the following goal

-- ...
new_s6 : Std.Slice Bool → Aeneas.Std.Array Bool 1600#usize
new_s6_post : ∀ (s : Std.Slice Bool), ↑(new_s6 s) = ↑(if h : (↑s).length = ↑1600#usize then ⟨↑s, h⟩ else mk_s5 s5)
-- ...
⊢ (Spec.Keccak.P 6 24 (BitVec.cast ⋯ (↑(new_s6 s6)).toBitVec)).toList.toBitVec.toNat =
  (absorb (BitVec.cast ⋯ (↑s).toBitVec)
      (Array.chunks_exact (↑r)
        ((↑rest ++ ↑suffix).toArray ++ Spec.«pad10*1» (↑r) ((↑rest).length + (↑suffix).length)))).toNat

In this case I'm unable to perform rw [new_s6_post s6]. I'll try to minimize the example after lunch, but it can probably be represented in my previous example by wrapping everything in another function call. I guess I could tweak all such functions to do away with the BitVecs and use Nats instead, but that would require that I do so for a bunch of definitions, and at that point I'd perhaps rather change the definitions themselves.

[Aaron Liu]

Can you use conv?

[Ayhon]

I tried to, but it gives a similar error about the motive not begin type correct.

Full error message

Diagnostics:
tactic 'rewrite' failed, motive is not type correct:
  fun _a => (Spec.Keccak.P 6 24 (BitVec.cast ⋯ _a.toBitVec)).toList.toBitVec
Error: application type mismatch
  Eq.trans (List.Vector.length_val (new_s6 s6))
argument
  List.Vector.length_val (new_s6 s6)
has type
  (↑(new_s6 s6)).length = ↑1600#usize : Prop
but is expected to have type
  _a.length = ↑1600#usize : Prop

Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' by the following process. First, it looks for all 'a' in 'e'. Second, it tries to abstract these occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, with the property that 'm a' is definitionally equal to 'e'. Third, we observe that 'congrArg' implies that 'm a = m b', which can be used with lemmas such as 'Eq.mpr' to change the goal. However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.

Possible solutions: use rewrite's 'occs' configuration option to limit which occurrences are rewritten, or use 'simp' or 'conv' mode, which have strategies for certain kinds of dependencies (these tactics can handle proofs and 'Decidable' instances whose types depend on the rewritten term, and 'simp' can apply user-defined '@[congr]' theorems as well).
rest suffix : Std.Slice Bool
r : Std.Usize
s : Aeneas.Std.Array Bool 1600#usize
r_pos : ↑r > 0
r_big_enough : ↑r ≥ 6
rest_lt : rest.length < ↑r
suffix_le : suffix.length ≤ 4
no_overflow : rest.length + suffix.length < Std.Usize.max
nb_left : Std.Usize
_✝¹⁶ : [> let nb_left ← rest.len + suffix.len <]
nb_left_post : ↑nb_left = ↑rest.len + ↑suffix.len
orig_s : Std.Slice Bool
mk_s1 : Std.Slice Bool → Aeneas.Std.Array Bool 1600#usize
_✝¹⁵ : [> let(orig_s, mk_s1) ← ↑s.to_slice_mut <]
orig_s_post : ↑orig_s = ↑s
mk_s1_post : ∀ (s_1 : Std.Slice Bool), ↑(mk_s1 s_1) = ↑(s.from_slice s_1)
s1 : Std.Slice Bool
_✝¹⁴ : [> let s1 ← xor_long orig_s rest <]
s1_val :
  (↑s1).toBitVec = BitVec.setWidth s1.length ((↑orig_s).toBitVec ^^^ BitVec.setWidth orig_s.length (↑rest).toBitVec)
s1_len : (↑s1).length = 1600
old_s1 : Std.Slice Bool
mk_s2 : Std.Slice Bool → Aeneas.Std.Array Bool 1600#usize
_✝¹³ : [> let(old_s1, mk_s2) ← ↑(mk_s1 s1).to_slice_mut <]
old_s1_post : ↑old_s1 = ↑(mk_s1 s1)
mk_s2_post : ∀ (s : Std.Slice Bool), ↑(mk_s2 s) = ↑((mk_s1 s1).from_slice s)
s2 : Std.Slice Bool
_✝¹² : [> let s2 ← xor_long_at old_s1 suffix rest.len <]
s2_val :
  ∀ j < old_s1.length,
    s2[j]! = if ↑rest.len ≤ j ∧ j < ↑rest.len + suffix.length then old_s1[j]! ^^ suffix[j - ↑rest.len]! else old_s1[j]!
s2_len : (↑s2).length = 1600
leftover : Std.Usize
_✝¹¹ : [> let leftover ← ↑(Std.core.num.Usize.saturating_sub nb_left r) <]
leftover_post : ↑leftover = ↑nb_left - ↑r
leftover_pos : leftover > 0#usize
s3 : Aeneas.Std.Array Bool 1600#usize
_✝¹⁰ : [> let s3 ← keccak_p (mk_s2 s2) <]
s3_val : ↑s3 = (Spec.Keccak.P 6 24 (BitVec.cast ⋯ (↑(mk_s2 s2)).toBitVec)).toList
s3_len : Spec.b 6 = 1600
old_s3 : Std.Slice Bool
mk_s4 : Std.Slice Bool → Aeneas.Std.Array Bool 1600#usize
_✝⁹ : [> let(old_s3, mk_s4) ← ↑s3.to_slice_mut <]
old_s3_post : ↑old_s3 = ↑s3
mk_s4_post : ∀ (s : Std.Slice Bool), ↑(mk_s4 s) = ↑(s3.from_slice s)
left : Std.Slice Bool
_✝⁸ :
  [> let left ←
    Std.core.slice.index.Slice.index (Std.core.slice.index.SliceIndexRangeFromUsizeSlice Bool) suffix
      { start := leftover } <]
left_post : ↑left = (↑suffix).extract ↑leftover
s4 : Std.Slice Bool
_✝⁷ : [> let s4 ← xor_long old_s3 left <]
s4_val : ↑s4 = List.zipWith xor ↑old_s3 ↑left ++ List.drop left.length ↑old_s3
s4_len : (↑s4).length = (↑s3).length
old_s4 : Std.Slice Bool
mk_s5 : Std.Slice Bool → Aeneas.Std.Array Bool 1600#usize
_✝⁶ : [> let(old_s4, mk_s5) ← ↑(mk_s4 s4).to_slice_mut <]
old_s4_post : ↑old_s4 = ↑(mk_s4 s4)
mk_s5_post : ∀ (s : Std.Slice Bool), ↑(mk_s5 s) = ↑((mk_s4 s4).from_slice s)
a_one : Std.Slice Bool
_✝⁵ : [> let a_one ← ↑(Std.Array.make 1#usize [true] proof_4).to_slice <]
a_one_post : a_one = ⟨↑(Std.Array.make 1#usize [true] proof_4), ⋯⟩
pos1 : Std.Usize
_✝⁴ : [> let pos1 ← suffix.len - leftover <]
pos1_post : ↑suffix.len = ↑pos1 + ↑leftover
s5 : Std.Slice Bool
_✝³ : [> let s5 ← xor_long_at old_s4 a_one pos1 <]
s5_len : (↑s5).length = 1600
s5_val :
  ∀ j < (↑old_s4).length,
    s5[j]! =
      if ↑pos1 ≤ j ∧ j < ↑pos1 + 1 then old_s4[j]! ^^ ⟨↑(Std.Array.make 1#usize [true] proof_4), ⋯⟩[j - ↑pos1]!
      else old_s4[j]!
old_s5 : Std.Slice Bool
new_s6 : Std.Slice Bool → Aeneas.Std.Array Bool 1600#usize
_✝² : [> let(old_s5, new_s6) ← ↑(mk_s5 s5).to_slice_mut <]
old_s5_post : ↑old_s5 = ↑(mk_s5 s5)
new_s6_post : ∀ (s : Std.Slice Bool), ↑(new_s6 s) = ↑(if h : (↑s).length = ↑1600#usize then ⟨↑s, h⟩ else mk_s5 s5)
pos2 : Std.Usize
_✝¹ : [> let pos2 ← r - 1#usize <]
pos2_post : ↑r = ↑pos2 + 1
s6 : Std.Slice Bool
_✝ : [> let s6 ← xor_long_at old_s5 a_one pos2 <]
s6_val :
  ∀ j < old_s5.length,
    s6[j]! = if ↑pos2 ≤ j ∧ j < ↑pos2 + a_one.length then old_s5[j]! ^^ a_one[j - ↑pos2]! else old_s5[j]!
s6_len : (↑s6).length = 1600
res : Aeneas.Std.Array Bool 1600#usize
_ : [> let res ← keccak_p (new_s6 s6) <]
res_len : res.length = (new_s6 s6).length
res_val : ↑res = (Spec.Keccak.P 6 24 (BitVec.cast ⋯ (↑(new_s6 s6)).toBitVec)).toList
| (Spec.Keccak.P 6 24 (BitVec.cast ⋯ (↑(new_s6 s6)).toBitVec)).toList.toBitVec

[Aaron Liu]

Where did you conv to?

[Aaron Liu]

You should enter the BitVec.cast.

[Aaron Liu]

Then you can use docs#apply_dite to push the cast through.

[Ayhon]

Fair enough. I actually didn't go as deep as I originally wanted to, since conv gives me an error when I try to go past the BitVec.cast.

[Aaron Liu]

This is a deficiency in conv then

[Aaron Liu]

specifically, a missing conv lemma

[Ayhon]

I see. If I understood correctly, the issue is that when trying to perform the rewriting, rw by default abstracts away too much, which we can regulate with conv, but since I have not extended conv with the appropiate lemmas, it's unable to do so. Correct?

Could the previous case also be solved by using conv instead of applying BitVec.toNat_eq?

[Ayhon]

Furthermore, I didn't know about conv lemmas, I'll have a look at that

[Aaron Liu]

Wait, which argument are you entering? I might have misinterpreted the error message.

[Aaron Liu]

This would be so much easier with a #mwe

[Aaron Liu]

Ok clearly the problem is with List.toBitVec, which I can't find any reference for and so I must assume you defined that function. What's it's type?

[Ayhon]

Yes, I'll work on a MWE. It just takes me a bit of time since there's a bunch of definitions I have to abstract over.

I was trying to enter the first argument, which would perform the following (in my head)

(Spec.Keccak.P 6 24 (BitVec.cast ⋯ (↑(new_s6 s6)).toBitVec)).toList.toBitVec
 ↓
(Spec.Keccak.P 6 24 (BitVec.cast ⋯ (↑(new_s6 s6)).toBitVec)).toList

[Aaron Liu]

What's the type of List.toBitVec?

[Ayhon]

Aaron Liu said:

Ok clearly the problem is with List.toBitVec, which I can't find any reference for and so I must assume you defined that function. What's it's type?

Yes, sorry, this whole situation is happening inside a project with a bunch of definitions. This one in particular

 abbrev List.toBitVec(self: List Bool): BitVec self.length := BitVec.ofBoolListLE self

[Ayhon]

And BitVec.ofBoolListLE is in Init. I just wanted the postfix notation

[Aaron Liu]

You'll probably have to write an explicit substitution motive then

[Ayhon]

I'm unsure of how to do this. Looking over at the code in conv, is this the part specified after the in? I can't see anything in the page about conv in TPiL, but the language reference makes it seem to me that it's not its purpose.

[Aaron Liu]

Like refine Eq.rec (motive := fun a h => explicit_motive) ?_ prf

[Ayhon]

Ah, I see, fully manually

[Aaron Liu]

The reason is you have to introduce a cast and rewrite half of it, which is probably too complicated for existing tactics.

[Ayhon]

Sorry, I have difficulty following with this last part. I'll try to reduce to a MWE to make it easier for me to follow.

Also, I see no reference to conv lemmas. Are there any examples of custom conv lemmas anywhere I could have a look at?

[Aaron Liu]

I think conv uses the simp-congr lemmas

[Ayhon]

I was thinking that perhaps instead of changing the motive I could change the equality I wanted to use. Instead of rewriting ↑(new_s6 s6) = ... I could transform this one to BitVec.cast pf (↑(new_s6 s6)).toBitVec = BitVec.cast pf (...).toBitVec using congrArg.

However, congrArg (f := List.toBitVec) doesn't seem to work in this case.

Error message

Diagnostics:
application type mismatch
  congrArg List.toBitVec
argument
  List.toBitVec
has type
  (self : List Bool) → BitVec self.length : Type
but is expected to have type
  List Bool → ?m.1251537 : Sort (imax 1 ?u.1251534)

However, this doesn't work because if a = b and f: (n: Nat) → BitVec n then f a : BitVec a, f b: BitVec b and so f a = f b is not type correct. I guess then that the congr lemma would be (h: a = b) → f a = (f b).cast h, but I see what I cannot define it as congr since it requires for the first function application to be the same.

With an auxiliary lemma, I've been able to perform the rewriting of (↑(new_s6 s6)).toBitVector.cast pf
by transforming

↑(new_s6 s6) = ...
    ↓
(↑(new_s6 s6)).toBitVector = (...).toBitVector.cast pf'
    ↓
(↑(new_s6 s6)).toBitVector.cast pf  = ((...).toBitVector.cast pf').cast pf

and then performing the rewriting.

However, the process was a bit involved. Ideally I'd like to be able to automate it, maybe by making more use of HEq? Would this scale?

[Aaron Liu]

I can think of how this can be automated

[Ayhon]

Aaron Liu said:

I can think of how this can be automated

Is this possible with the current tactics, or simply implementable as a new tactic?

[Aaron Liu]

I mean as a new tactic, but I guess you could patch together a curated simp set with some congr