Skip to content

Commit

Permalink
Fixing initial value for indexing variables in AESArm and fix CSE gua…
Browse files Browse the repository at this point in the history 
…rd_msgs
  • Loading branch information
@pennyannn
pennyannn committed Sep 27, 2024
1 parent 612d9b5 commit 61af51a
Show file tree
Hide file tree
Showing 3 changed files with 135 additions and 138 deletions.
4 changes: 2 additions & 2 deletions Specs/AESArm.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ protected def KeyExpansion_helper {Param : KBR} (i : Nat) (ks : KeySchedule)
def KeyExpansion {Param : KBR} (key : BitVec Param.key_len)
: KeySchedule :=
let seeded := AESArm.InitKey (Param := Param) Param.Nk key []
AESArm.KeyExpansion_helper (Param := Param) Param.Nk seeded
AESArm.KeyExpansion_helper (Param := Param) (4 * Param.Nr + 4 - Param.Nk) seeded

def SubBytes {Param : KBR} (state : BitVec Param.block_size)
: BitVec Param.block_size :=
Expand Down Expand Up @@ -227,7 +227,7 @@ def AES_encrypt_with_ks {Param : KBR} (input : BitVec Param.block_size)
-- have h₀ : WordSize + WordSize + WordSize + WordSize = Param.block_size := by
-- simp only [WordSize, BlockSize, Param.h]
let state := AddRoundKey input $ (AESArm.getKey 0 w)
let state := AESArm.AES_encrypt_with_ks_loop (Param := Param) 1 state w
let state := AESArm.AES_encrypt_with_ks_loop (Param := Param) (Param.Nr - 1) state w
let state := SubBytes (Param := Param) state
let state := ShiftRows (Param := Param) state
AddRoundKey state $ AESArm.getKey Param.Nr w
Expand Down
2 changes: 2 additions & 0 deletions Specs/AESV8.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -111,6 +111,8 @@ def AESHWCtr32EncryptBlocks_helper {Param : AESArm.KBR} (in_blocks : BitVec m)
if i >= len then acc
else
let lo := m - (i + 1) * 128
let hi := lo + 127
have h5 : hi - lo + 1 = 128 := by omega
let curr_block : BitVec 128 := BitVec.extractLsb' lo 128 in_blocks
have h4 : 128 = Param.block_size := by
cases h3
Expand Down
267 changes: 131 additions & 136 deletions Tests/Tactics/CSE.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -260,10 +260,9 @@ warning: declaration uses 'sorry'
---
info: H : 64 > 0
a b c d e : BitVec 128
x1 x2 : BitVec 64
x3 : BitVec (127 - 64 + 1)
x1 x2 x3 : BitVec 64
x4 : BitVec 128
hx3 : BitVec.extractLsb 127 64 x4 = x3
hx3 : BitVec.extractLsb' 64 64 x4 = x3
x5 x6 x7 x8 x9 : BitVec 64
hx2 : x9 + x3 = x2
x10 x11 : BitVec 128
Expand All @@ -273,14 +272,13 @@ hx10 : x12 &&& 18446744073709551615#128 = x10
x13 : BitVec 128
hx11 : x13 <<< 64 = 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
x16 : BitVec (63 - 0 + 1)
x17 : BitVec (127 - 64 + 1)
hx12 : BitVec.zeroExtend 128 x15 = x12
x16 x17 : BitVec 64
x18 : BitVec 128
hx16 : BitVec.extractLsb 63 0 x18 = x16
hx17 : BitVec.extractLsb 127 64 x18 = x17
hx16 : BitVec.extractLsb' 64 64 x18 = x16
hx17 : BitVec.extractLsb' 0 64 x18 = x17
x19 x20 : BitVec 64
hx8 : x19 + x20 = x8
x21 : BitVec 64
Expand All @@ -289,78 +287,78 @@ x22 : BitVec 128
x23 : BitVec 64
x24 : BitVec 128
hx18 : x22 ||| x24 = x18
x25 : BitVec 64
x26 : BitVec 128
hx22 : x26 &&& 18446744073709551615#128 = x22
x25 : BitVec 128
hx22 : x25 &&& 18446744073709551615#128 = x22
x26 : BitVec 64
x27 : BitVec 128
hx24 : x27 <<< 64 = x24
x28 : BitVec 64
hx27 : BitVec.zeroExtend 128 x28 = x27
x29 : BitVec 64
hx20 : x29 ^^^ x25 = x20
hx25 : BitVec.zeroExtend 128 x29 = x25
x30 : BitVec 64
hx26 : BitVec.zeroExtend 128 x30 = x26
hx20 : x30 ^^^ x26 = x20
x31 x32 : BitVec 64
hx23 : x31 ^^^ x32 = x23
hx21 : x23 ^^^ x32 = x21
x33 x34 : BitVec 64
hx21 : x23 ^^^ x34 = x21
x35 : BitVec (127 - 64 + 1)
hx35 : BitVec.extractLsb 127 64 d = x35
hx7 : x8 + x35 = x7
x36 : BitVec (63 - 0 + 1)
hx36 : BitVec.extractLsb 63 0 a = x36
x37 : BitVec (63 - 0 + 1)
hx37 : BitVec.extractLsb 63 0 c = x37
x38 : BitVec (127 - 64 + 1)
hx38 : BitVec.extractLsb 127 64 c = x38
hx19 : x38 + x21 = x19
hx28 : x38 + x35 = x28
x39 : BitVec (127 - 64 + 1)
hx39 : BitVec.extractLsb 127 64 e = x39
hx6 : x7 + x39 = x6
hx15 : x17 + x39 = x15
x40 : BitVec (63 - 0 + 1)
hx40 : BitVec.extractLsb 63 0 b = x40
hx1 : x2 + x40 = x1
hx5 : x40 + x6 = x5
x41 : BitVec (63 - 0 + 1)
hx41 : BitVec.extractLsb 63 0 d = x41
hx30 : x37 + x41 = x30
x42 : BitVec (127 - 64 + 1)
hx42 : BitVec.extractLsb 127 64 a = x42
hx25 : x33 &&& x42 = x25
x43 : BitVec (127 - 64 + 1)
hx43 : BitVec.extractLsb 127 64 b = x43
hx31 : x43.rotateRight 14 = x31
hx32 : x43.rotateRight 18 = x32
hx33 : ~~~x43 = x33
hx34 : x43.rotateRight 41 = x34
hx29 : x43 &&& x36 = x29
x44 : BitVec (63 - 0 + 1)
hx44 : BitVec.extractLsb 63 0 e = x44
hx14 : x16 + x44 = x14
hx23 : x31 ^^^ x34 = x23
x35 : BitVec 64
hx35 : BitVec.extractLsb' 0 64 a = x35
x36 : BitVec 64
hx36 : BitVec.extractLsb' 0 64 c = x36
x37 : BitVec 64
hx37 : BitVec.extractLsb' 0 64 b = x37
hx1 : x2 + x37 = x1
hx5 : x37 + x6 = x5
x38 : BitVec 64
hx38 : BitVec.extractLsb' 64 64 e = x38
hx6 : x7 + x38 = x6
hx14 : x16 + x38 = x14
x39 : BitVec 64
hx39 : BitVec.extractLsb' 64 64 a = x39
hx26 : x33 &&& x39 = x26
x40 : BitVec 64
hx40 : BitVec.extractLsb' 64 64 b = x40
hx31 : x40.rotateRight 14 = x31
hx32 : x40.rotateRight 41 = x32
hx33 : ~~~x40 = x33
hx34 : x40.rotateRight 18 = x34
hx30 : x40 &&& x35 = x30
x41 : BitVec 64
hx41 : BitVec.extractLsb' 64 64 d = x41
hx7 : x8 + x41 = x7
x42 : BitVec 64
hx42 : BitVec.extractLsb' 64 64 c = x42
hx19 : x42 + x21 = x19
hx28 : x42 + x41 = x28
x43 : BitVec 64
hx43 : BitVec.extractLsb' 0 64 d = x43
hx29 : x36 + x43 = x29
x44 : BitVec 64
hx44 : BitVec.extractLsb' 0 64 e = x44
hx15 : x17 + x44 = x15
⊢ x2 ++
((x1 &&& x43 ^^^ ~~~x1 &&& x36) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
BitVec.extractLsb 63 0 x4) =
((x1 &&& x40 ^^^ ~~~x1 &&& x35) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
BitVec.extractLsb' 0 64 x4) =
x6 ++
(x37 + (x5.rotateRight 14 ^^^ x5.rotateRight 18 ^^^ x5.rotateRight 41) + (x5 &&& x43 ^^^ ~~~x5 &&& x36) + x41 +
(x36 + (x5.rotateRight 14 ^^^ x5.rotateRight 18 ^^^ x5.rotateRight 41) + (x5 &&& x40 ^^^ ~~~x5 &&& x35) + x43 +
x44)
-/
#guard_msgs in theorem sha512h_rule_1 (a b c d e : BitVec 128) :
let elements := 2
let esize := 64
let inner_sum := (binary_vector_op_aux 0 elements esize BitVec.add c d (BitVec.zero 128) H)
let outer_sum := (binary_vector_op_aux 0 elements esize BitVec.add inner_sum e (BitVec.zero 128) H)
let a0 := extractLsb 63 0 a
let a1 := extractLsb 127 64 a
let b0 := extractLsb 63 0 b
let b1 := extractLsb 127 64 b
let c0 := extractLsb 63 0 c
let c1 := extractLsb 127 64 c
let d0 := extractLsb 63 0 d
let d1 := extractLsb 127 64 d
let e0 := extractLsb 63 0 e
let e1 := extractLsb 127 64 e
let a0 := extractLsb' 0 64 a
let a1 := extractLsb' 64 64 a
let b0 := extractLsb' 0 64 b
let b1 := extractLsb' 64 64 b
let c0 := extractLsb' 0 64 c
let c1 := extractLsb' 64 64 c
let d0 := extractLsb' 0 64 d
let d1 := extractLsb' 64 64 d
let e0 := extractLsb' 0 64 e
let e1 := extractLsb' 64 64 e
let hi64_spec := compression_update_t1 b1 a0 a1 c1 d1 e1
let lo64_spec := compression_update_t1 (b0 + hi64_spec) b1 a0 c0 d0 e0
sha512h a b outer_sum = hi64_spec ++ lo64_spec := by
Expand All @@ -385,28 +383,25 @@ warning: declaration uses 'sorry'
---
info: h1 h2 : 64 > 0
a b c d e : BitVec 128
x1 x2 : BitVec 64
x3 : BitVec (127 - 64 + 1)
x1 x2 x3 : BitVec 64
x4 : BitVec 128
hx3 : BitVec.extractLsb 127 64 x4 = x3
hx3 : BitVec.extractLsb' 64 64 x4 = x3
x5 : BitVec 64
x6 x7 : BitVec 128
hx4 : x7 ||| x6 = x4
hx6 : x7 <<< 64 = x6
x8 : BitVec 128
hx6 : x8 <<< 64 = x6
hx4 : x8 ||| x6 = x4
x9 : BitVec 64
hx7 : BitVec.zeroExtend 128 x9 = x7
x10 : BitVec 64
hx8 : BitVec.zeroExtend 128 x10 = x8
x11 : BitVec 64
x12 : BitVec (127 - 64 + 1)
x13 : BitVec (63 - 0 + 1)
x14 : BitVec 64
x15 : BitVec (191 - 64 + 1)
hx12 : BitVec.extractLsb 127 64 x15 = x12
hx13 : BitVec.extractLsb 63 0 x15 = x13
x11 x12 x13 : BitVec 64
x14 : BitVec 128
hx12 : BitVec.extractLsb' 64 64 x14 = x12
hx13 : BitVec.extractLsb' 0 64 x14 = x13
x15 : BitVec 64
x16 : BitVec 256
hx15 : BitVec.extractLsb 191 64 x16 = x15
hx14 : BitVec.extractLsb' 64 128 x16 = x14
x17 x18 : BitVec 64
hx2 : x18 + x3 = x2
x19 : BitVec 128
Expand All @@ -418,75 +413,75 @@ hx18 : x21 + x22 = x18
x23 : BitVec 128
x24 : BitVec 64
x25 : BitVec 128
hx19 : x25 ||| x23 = x19
hx23 : x25 <<< 64 = x23
x26 : BitVec 128
hx23 : x26 <<< 64 = x23
hx19 : x26 ||| x23 = x19
x27 x28 : BitVec 64
hx25 : BitVec.zeroExtend 128 x28 = x25
hx21 : x28 ^^^ x27 = x21
x29 : BitVec 64
hx26 : BitVec.zeroExtend 128 x29 = x26
hx25 : BitVec.zeroExtend 128 x29 = x25
x30 : BitVec 64
hx21 : x30 ^^^ x27 = x21
x31 : BitVec 64
hx22 : x24 ^^^ x31 = x22
x32 x33 x34 : BitVec 64
hx24 : x33 ^^^ x34 = x24
x35 : BitVec (63 - 0 + 1)
hx35 : BitVec.extractLsb 63 0 b = x35
hx1 : x2 + x35 = x1
hx5 : x35 + x11 = x5
x36 : BitVec (63 - 0 + 1)
hx36 : BitVec.extractLsb 63 0 a = x36
x37 : BitVec (127 - 64 + 1)
hx37 : BitVec.extractLsb 127 64 b = x37
hx31 : x37.rotateRight 41 = x31
hx32 : ~~~x37 = x32
hx33 : x37.rotateRight 14 = x33
hx34 : x37.rotateRight 18 = x34
hx30 : x37 &&& x36 = x30
x38 : BitVec (127 - 64 + 1)
hx38 : BitVec.extractLsb 127 64 a = x38
hx27 : x32 &&& x38 = x27
x39 : BitVec (127 - 64 + 1)
hx39 : BitVec.extractLsb 127 64 e = x39
x40 : BitVec (63 - 0 + 1)
hx40 : BitVec.extractLsb 63 0 c = x40
hx9 : x40 + x13 = x9
x41 : BitVec (127 - 64 + 1)
hx41 : BitVec.extractLsb 127 64 d = x41
hx29 : x41 + x39 = x29
x42 : BitVec (63 - 0 + 1)
hx42 : BitVec.extractLsb 63 0 e = x42
hx11 : x14 + x42 = x11
x43 : BitVec (127 - 64 + 1)
hx43 : BitVec.extractLsb 127 64 c = x43
hx10 : x43 + x12 = x10
hx20 : x43 + x22 = x20
x44 : BitVec (63 - 0 + 1)
hx44 : BitVec.extractLsb 63 0 d = x44
hx14 : x17 + x44 = x14
hx28 : x44 + x42 = x28
hx26 : BitVec.zeroExtend 128 x30 = x26
x31 x32 : BitVec 64
hx24 : x32 ^^^ x31 = x24
x33 : BitVec 64
hx22 : x24 ^^^ x33 = x22
x34 x35 : BitVec 64
hx35 : BitVec.extractLsb' 64 64 a = x35
hx27 : x34 &&& x35 = x27
x36 : BitVec 64
hx36 : BitVec.extractLsb' 0 64 a = x36
x37 : BitVec 64
hx37 : BitVec.extractLsb' 0 64 e = x37
hx11 : x15 + x37 = x11
x38 : BitVec 64
hx38 : BitVec.extractLsb' 64 64 d = x38
x39 : BitVec 64
hx39 : BitVec.extractLsb' 0 64 b = x39
hx1 : x2 + x39 = x1
hx5 : x39 + x11 = x5
x40 : BitVec 64
hx40 : BitVec.extractLsb' 0 64 c = x40
hx10 : x40 + x13 = x10
x41 : BitVec 64
hx41 : BitVec.extractLsb' 64 64 e = x41
hx29 : x38 + x41 = x29
x42 : BitVec 64
hx42 : BitVec.extractLsb' 64 64 b = x42
hx31 : x42.rotateRight 18 = x31
hx32 : x42.rotateRight 14 = x32
hx33 : x42.rotateRight 41 = x33
hx34 : ~~~x42 = x34
hx28 : x42 &&& x36 = x28
x43 : BitVec 64
hx43 : BitVec.extractLsb' 0 64 d = x43
hx15 : x17 + x43 = x15
hx30 : x43 + x37 = x30
x44 : BitVec 64
hx44 : BitVec.extractLsb' 64 64 c = x44
hx9 : x44 + x12 = x9
hx20 : x44 + x22 = x20
⊢ x2 ++
((x1 &&& x37 ^^^ ~~~x1 &&& x36) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
BitVec.extractLsb 63 0 x4) =
((x1 &&& x42 ^^^ ~~~x1 &&& x36) + (x1.rotateRight 14 ^^^ x1.rotateRight 18 ^^^ x1.rotateRight 41) +
BitVec.extractLsb' 0 64 x4) =
x11 ++
(x40 + (x5.rotateRight 14 ^^^ x5.rotateRight 18 ^^^ x5.rotateRight 41) + (x5 &&& x37 ^^^ ~~~x5 &&& x36) + x41 +
x39)
(x40 + (x5.rotateRight 14 ^^^ x5.rotateRight 18 ^^^ x5.rotateRight 41) + (x5 &&& x42 ^^^ ~~~x5 &&& x36) + x38 +
x41)
-/
#guard_msgs in theorem sha512h_rule_2 (a b c d e : BitVec 128) :
let a0 := extractLsb 63 0 a
let a1 := extractLsb 127 64 a
let b0 := extractLsb 63 0 b
let b1 := extractLsb 127 64 b
let c0 := extractLsb 63 0 c
let c1 := extractLsb 127 64 c
let d0 := extractLsb 63 0 d
let d1 := extractLsb 127 64 d
let e0 := extractLsb 63 0 e
let e1 := extractLsb 127 64 e
let a0 := extractLsb' 0 64 a
let a1 := extractLsb' 64 64 a
let b0 := extractLsb' 0 64 b
let b1 := extractLsb' 64 64 b
let c0 := extractLsb' 0 64 c
let c1 := extractLsb' 64 64 c
let d0 := extractLsb' 0 64 d
let d1 := extractLsb' 64 64 d
let e0 := extractLsb' 0 64 e
let e1 := extractLsb' 64 64 e
let inner_sum := binary_vector_op_aux 0 2 64 BitVec.add d e (BitVec.zero 128) h1
let concat := inner_sum ++ inner_sum
let operand := extractLsb 191 64 concat
let operand := extractLsb' 64 128 concat
let hi64_spec := compression_update_t1 b1 a0 a1 c1 d0 e0
let lo64_spec := compression_update_t1 (b0 + hi64_spec) b1 a0 c0 d1 e1
sha512h a b (binary_vector_op_aux 0 2 64 BitVec.add c operand (BitVec.zero 128) h2) =
Expand Down

0 comments on commit 61af51a

Please sign in to comment.