Skip to content

Commit

Permalink
chore: update CSE
Browse files Browse the repository at this point in the history
  • Loading branch information
@bollu
bollu committed Nov 1, 2024
1 parent 4bc6d6c commit d18b599
Showing 1 changed file with 90 additions and 92 deletions.
182 changes: 90 additions & 92 deletions Tests/Tactics/CSE.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,10 +64,8 @@ hx1 : x2 <<< 64 = x1
x3 : BitVec 64
hx3 : BitVec.extractLsb' 64 64 c = x3
hx2 : BitVec.zeroExtend 128 x3 = x2
⊢ BitVec.zeroExtend 128 (BitVec.extractLsb' 0 64 x1) ||| BitVec.zeroExtend 128 (BitVec.extractLsb' 64 64 x1) =
sorryAx (BitVec 128)
⊢ BitVec.zeroExtend 128 (BitVec.extractLsb' 0 64 x1) ||| BitVec.zeroExtend 128 (BitVec.extractLsb' 64 64 x1) = sorry
-/

#guard_msgs in theorem bitvec_subexpr (a b c d : BitVec 64) : (zeroExtend 128
(extractLsb' 0 64
(
Expand Down Expand Up @@ -95,13 +93,13 @@ hx2 : x9 + x3 = x2
x10 x11 : BitVec 128
hx4 : x11 ||| x10 = x4
x12 : BitVec 128
hx11 : x12 &&& 18446744073709551615#128 = x11
hx10 : x12 <<< 64 = x10
x13 : BitVec 128
hx10 : x13 <<< 64 = x10
hx11 : x13 &&& 18446744073709551615#128 = x11
x14 : BitVec 64
hx12 : BitVec.zeroExtend 128 x14 = x12
hx13 : BitVec.zeroExtend 128 x14 = x13
x15 : BitVec 64
hx13 : BitVec.zeroExtend 128 x15 = x13
hx12 : BitVec.zeroExtend 128 x15 = x12
x16 x17 : BitVec 64
x18 : BitVec 128
hx16 : BitVec.extractLsb' 64 64 x18 = x16
Expand All @@ -112,62 +110,62 @@ x21 : BitVec 64
hx9 : x20 + x21 = x9
x22 : BitVec 64
x23 x24 : BitVec 128
hx18 : x24 ||| x23 = x18
x25 : BitVec 128
hx23 : x25 <<< 64 = x23
x26 : BitVec 64
hx18 : x23 ||| x24 = x18
x25 : BitVec 64
x26 : BitVec 128
hx24 : x26 <<< 64 = x24
x27 : BitVec 128
hx24 : x27 &&& 18446744073709551615#128 = x24
hx23 : x27 &&& 18446744073709551615#128 = x23
x28 : BitVec 64
hx20 : x28 ^^^ x26 = x20
hx20 : x28 ^^^ x25 = x20
x29 : BitVec 64
hx25 : BitVec.zeroExtend 128 x29 = x25
hx27 : BitVec.zeroExtend 128 x29 = x27
x30 : BitVec 64
hx27 : BitVec.zeroExtend 128 x30 = x27
x31 : BitVec 64
hx21 : x22 ^^^ x31 = x21
x32 x33 x34 : BitVec 64
hx22 : x34 ^^^ x33 = x22
hx26 : BitVec.zeroExtend 128 x30 = x26
x31 x32 x33 : BitVec 64
hx21 : x22 ^^^ x33 = x21
x34 : BitVec 64
hx22 : x34 ^^^ x32 = x22
x35 : BitVec 64
hx35 : BitVec.extractLsb' 64 64 a = x35
hx26 : x32 &&& x35 = x26
hx35 : BitVec.extractLsb' 64 64 e = x35
hx6 : x7 + x35 = x6
hx15 : x16 + x35 = x15
x36 : BitVec 64
hx36 : BitVec.extractLsb' 64 64 e = x36
hx6 : x7 + x36 = x6
hx15 : x16 + x36 = x15
hx36 : BitVec.extractLsb' 64 64 a = x36
hx25 : x31 &&& x36 = x25
x37 : BitVec 64
hx37 : BitVec.extractLsb' 0 64 a = x37
x38 : BitVec 64
hx38 : BitVec.extractLsb' 64 64 d = x38
hx7 : x8 + x38 = x7
hx38 : BitVec.extractLsb' 0 64 d = x38
x39 : BitVec 64
hx39 : BitVec.extractLsb' 0 64 c = x39
hx39 : BitVec.extractLsb' 64 64 c = x39
hx19 : x39 + x21 = x19
x40 : BitVec 64
hx40 : BitVec.extractLsb' 64 64 c = x40
hx19 : x40 + x21 = x19
hx29 : x40 + x38 = x29
hx40 : BitVec.extractLsb' 0 64 b = x40
hx1 : x2 + x40 = x1
hx5 : x40 + x6 = x5
x41 : BitVec 64
hx41 : BitVec.extractLsb' 0 64 b = x41
hx1 : x2 + x41 = x1
hx5 : x41 + x6 = x5
hx41 : BitVec.extractLsb' 64 64 b = x41
hx31 : ~~~x41 = x31
hx32 : x41.rotateRight 18 = x32
hx33 : x41.rotateRight 41 = x33
hx34 : x41.rotateRight 14 = x34
hx28 : x41 &&& x37 = x28
x42 : BitVec 64
hx42 : BitVec.extractLsb' 64 64 b = x42
hx31 : x42.rotateRight 41 = x31
hx32 : ~~~x42 = x32
hx33 : x42.rotateRight 18 = x33
hx34 : x42.rotateRight 14 = x34
hx28 : x42 &&& x37 = x28
hx42 : BitVec.extractLsb' 64 64 d = x42
hx7 : x8 + x42 = x7
hx30 : x39 + x42 = x30
x43 : BitVec 64
hx43 : BitVec.extractLsb' 0 64 e = x43
hx14 : x17 + x43 = x14
x44 : BitVec 64
hx44 : BitVec.extractLsb' 0 64 d = x44
hx30 : x39 + x44 = x30
hx44 : BitVec.extractLsb' 0 64 c = x44
hx29 : x44 + x38 = x29
⊢ x2 ++
((x1 &&& x42 ^^^ ~~~x1 &&& x37) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
((x1 &&& x41 ^^^ ~~~x1 &&& x37) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
BitVec.extractLsb' 0 64 x4) =
x6 ++
(x39 + (x5.rotateRight 14 ^^^ x5.rotateRight 18 ^^^ x5.rotateRight 41) + (x5 &&& x42 ^^^ ~~~x5 &&& x37) + x44 +
(x44 + (x5.rotateRight 14 ^^^ x5.rotateRight 18 ^^^ x5.rotateRight 41) + (x5 &&& x41 ^^^ ~~~x5 &&& x37) + x38 +
x43)
-/
#guard_msgs in theorem sha512h_rule_1 (a b c d e : BitVec 128) :
Expand All @@ -193,7 +191,7 @@ hx30 : x39 + x44 = x30
unfold BitVec.partInstall
unfold sha512h compression_update_t1 sigma_big_1 ch allOnes ror
simp only [Nat.reduceAdd, Nat.reduceSub, Nat.sub_zero, Nat.reducePow, reduceZeroExtend,
reduceHShiftLeft, reduceNot, reduceAnd, BitVec.zero_or, shiftLeft_zero_eq]
reduceHShiftLeft, reduceNot, reduceAnd, BitVec.zero_or, shiftLeft_zero]
cse (config := { minOccsToCSE := 2, fuelSearch := 99999, fuelEliminate := 99999 })
trace_state
all_goals sorry
Expand All @@ -214,85 +212,85 @@ hx3 : BitVec.extractLsb' 64 64 x4 = x3
x5 : BitVec 128
x6 : BitVec 64
x7 : BitVec 128
hx4 : x7 ||| x5 = x4
hx5 : x7 <<< 64 = x5
x8 : BitVec 128
hx5 : x8 <<< 64 = x5
hx4 : x8 ||| x5 = x4
x9 : BitVec 64
hx8 : BitVec.zeroExtend 128 x9 = x8
x10 : BitVec 64
hx7 : BitVec.zeroExtend 128 x10 = x7
x11 x12 x13 x14 : BitVec 64
x15 : BitVec 128
hx12 : BitVec.extractLsb' 64 64 x15 = x12
hx13 : BitVec.extractLsb' 0 64 x15 = x13
x11 x12 x13 : BitVec 64
x14 : BitVec 128
hx12 : BitVec.extractLsb' 0 64 x14 = x12
hx13 : BitVec.extractLsb' 64 64 x14 = x13
x15 : BitVec 64
x16 : BitVec 256
hx15 : BitVec.extractLsb' 64 128 x16 = x15
hx14 : BitVec.extractLsb' 64 128 x16 = x14
x17 x18 : BitVec 64
hx2 : x18 + x3 = x2
x19 : BitVec 128
hx16 : x19 ++ x19 = x16
x20 x21 : BitVec 64
hx17 : x20 + x21 = x17
x19 : BitVec 64
x20 : BitVec 128
hx16 : x20 ++ x20 = x16
x21 : BitVec 64
hx17 : x19 + x21 = x17
x22 : BitVec 64
hx18 : x21 + x22 = x18
x23 : BitVec 64
x24 : BitVec 128
x25 : BitVec 64
x24 x25 : BitVec 128
hx20 : x25 ||| x24 = x20
x26 : BitVec 128
hx24 : x26 <<< 64 = x24
x27 : BitVec 128
hx19 : x27 ||| x24 = x19
x28 : BitVec 64
hx21 : x28 ^^^ x25 = x21
x27 x28 : BitVec 64
hx21 : x28 ^^^ x27 = x21
x29 : BitVec 64
hx26 : BitVec.zeroExtend 128 x29 = x26
hx25 : BitVec.zeroExtend 128 x29 = x25
x30 : BitVec 64
hx27 : BitVec.zeroExtend 128 x30 = x27
x31 x32 : BitVec 64
hx22 : x23 ^^^ x32 = x22
x33 : BitVec 64
hx23 : x33 ^^^ x31 = x23
x34 x35 : BitVec 64
hx26 : BitVec.zeroExtend 128 x30 = x26
x31 : BitVec 64
hx22 : x23 ^^^ x31 = x22
x32 x33 x34 : BitVec 64
hx23 : x34 ^^^ x32 = x23
x35 : BitVec 64
hx35 : BitVec.extractLsb' 0 64 b = x35
hx1 : x2 + x35 = x1
hx6 : x35 + x11 = x6
x36 : BitVec 64
hx36 : BitVec.extractLsb' 64 64 b = x36
hx31 : x36.rotateRight 18 = x31
hx32 : x36.rotateRight 41 = x32
hx33 : x36.rotateRight 14 = x33
hx34 : ~~~x36 = x34
hx36 : BitVec.extractLsb' 0 64 d = x36
hx15 : x17 + x36 = x15
x37 : BitVec 64
hx37 : BitVec.extractLsb' 64 64 e = x37
hx37 : BitVec.extractLsb' 64 64 d = x37
x38 : BitVec 64
hx38 : BitVec.extractLsb' 64 64 d = x38
hx29 : x38 + x37 = x29
hx38 : BitVec.extractLsb' 64 64 c = x38
hx10 : x38 + x13 = x10
hx19 : x38 + x22 = x19
x39 : BitVec 64
hx39 : BitVec.extractLsb' 64 64 c = x39
hx39 : BitVec.extractLsb' 0 64 c = x39
hx9 : x39 + x12 = x9
hx20 : x39 + x22 = x20
x40 : BitVec 64
hx40 : BitVec.extractLsb' 0 64 d = x40
hx14 : x17 + x40 = x14
hx40 : BitVec.extractLsb' 0 64 a = x40
x41 : BitVec 64
hx41 : BitVec.extractLsb' 0 64 c = x41
hx10 : x41 + x13 = x10
hx41 : BitVec.extractLsb' 64 64 e = x41
hx30 : x37 + x41 = x30
x42 : BitVec 64
hx42 : BitVec.extractLsb' 0 64 a = x42
hx28 : x36 &&& x42 = x28
hx42 : BitVec.extractLsb' 0 64 e = x42
hx11 : x15 + x42 = x11
hx29 : x36 + x42 = x29
x43 : BitVec 64
hx43 : BitVec.extractLsb' 0 64 e = x43
hx11 : x14 + x43 = x11
hx30 : x40 + x43 = x30
hx43 : BitVec.extractLsb' 64 64 b = x43
hx31 : x43.rotateRight 41 = x31
hx32 : x43.rotateRight 18 = x32
hx33 : ~~~x43 = x33
hx34 : x43.rotateRight 14 = x34
hx28 : x43 &&& x40 = x28
x44 : BitVec 64
hx44 : BitVec.extractLsb' 64 64 a = x44
hx25 : x34 &&& x44 = x25
hx27 : x33 &&& x44 = x27
⊢ x2 ++
((x1 &&& x36 ^^^ ~~~x1 &&& x42) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
((x1 &&& x43 ^^^ ~~~x1 &&& x40) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
BitVec.extractLsb' 0 64 x4) =
x11 ++
(x41 + (x6.rotateRight 14 ^^^ x6.rotateRight 18 ^^^ x6.rotateRight 41) + (x6 &&& x36 ^^^ ~~~x6 &&& x42) + x38 +
x37)
(x39 + (x6.rotateRight 14 ^^^ x6.rotateRight 18 ^^^ x6.rotateRight 41) + (x6 &&& x43 ^^^ ~~~x6 &&& x40) + x37 +
x41)
-/
#guard_msgs in theorem sha512h_rule_2 (a b c d e : BitVec 128) :
let a0 := extractLsb' 0 64 a
Expand All @@ -318,7 +316,7 @@ hx25 : x34 &&& x44 = x25
simp only [Nat.reduceAdd, Nat.reduceSub, Nat.reduceMul, Nat.sub_zero, reduceAllOnes,
reduceZeroExtend, Nat.zero_mul, reduceHShiftLeft, reduceNot, reduceAnd, Nat.one_mul,
BitVec.cast_eq]
simp only [shiftLeft_zero_eq, BitVec.zero_or, and_nop_lemma]
simp only [shiftLeft_zero, BitVec.zero_or, and_nop_lemma]
cse (config := {fuelSearch := 999999, fuelEliminate := 999999})
trace_state
all_goals sorry
Expand Down

0 comments on commit d18b599

Please sign in to comment.