-
Notifications
You must be signed in to change notification settings - Fork 18
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Make AES_KW(P) proofs more self-contained
This patch ensures that the AES_KW(P) proof developments all use files that are isolated from the proof developments for AES (previously, the former depended on the latter). In a subsequent commit, we will modify the AES proof developments to support unbounded AES-GCM, and we want to ensure that changes to AES do not interfere with the proofs for AES_KW(P).
- Loading branch information
1 parent
ebe9626
commit 34892fe
Showing
6 changed files
with
494 additions
and
8 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,178 @@ | ||
| /* | ||
| * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
| * SPDX-License-Identifier: Apache-2.0 | ||
| */ | ||
|
|
||
| // Using experimental proof command "crucible_llvm_verify_x86" | ||
| enable_experimental; | ||
|
|
||
|
|
||
| //////////////////////////////////////////////////////////////////////////////// | ||
| // Specifications | ||
|
|
||
| let AES_BLOCK_SIZE = 16; | ||
| let aes_key_len = 32; | ||
| // the number of AES rounds excluding the initial round and the final round | ||
| let aes_rounds = 13; | ||
|
|
||
|
|
||
| let fresh_aes_key_st = do { | ||
| crucible_fresh_var "key" (llvm_array aes_key_len (llvm_int 8)); | ||
| }; | ||
|
|
||
| let points_to_aes_key_st ptr key = do { | ||
| crucible_points_to_untyped ptr (crucible_struct [(crucible_term {{ key }}), crucible_term ({{ aes_key_from_schedule (ExpandKey (join key)) }}), (crucible_term {{ `aes_rounds : [32] }})]); | ||
| }; | ||
|
|
||
| // Some specs manipulate the blocks of the key, it is useful to represent the key as a pair of blocks. | ||
| let fresh_aes_key_256_parts = do { | ||
| low <- crucible_fresh_var "key_low" (llvm_array (eval_size {|aes_key_len/2|}) (llvm_int 8)); | ||
| high <- crucible_fresh_var "key_high" (llvm_array (eval_size {|aes_key_len/2|}) (llvm_int 8)); | ||
| return (low,high); | ||
| }; | ||
|
|
||
| // For AES decrypt, the round keys are stored in memory in reverse order. | ||
| let points_to_inv_aes_key_st ptr (low,high) = do { | ||
| crucible_points_to (crucible_elem ptr 1) (crucible_term {{ `aes_rounds : [32] }}); | ||
|
|
||
| crucible_points_to_untyped (crucible_elem (crucible_elem ptr 0) 0) (crucible_term {{ (inv_aes_key_from_schedule (ExpandKey (join (low#high))))}}); | ||
|
|
||
| crucible_points_to_untyped (crucible_elem (crucible_elem ptr 0) (eval_size {|4 *13 |})) (crucible_term high); | ||
| crucible_points_to_untyped (crucible_elem (crucible_elem ptr 0) (eval_size {|4 *14 |})) (crucible_term low); | ||
| }; | ||
|
|
||
| let aes_hw_set_encrypt_key_spec = do { | ||
| global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
|
|
||
| (user_key, user_key_ptr) <- ptr_to_fresh_readonly "user_key" (llvm_array aes_key_len (llvm_int 8)); | ||
| key_ptr <- crucible_alloc (llvm_struct "struct.aes_key_st"); | ||
|
|
||
| let bits = eval_size {| aes_key_len * 8 |}; | ||
| crucible_execute_func [user_key_ptr, (crucible_term {{ `bits : [32] }}), key_ptr]; | ||
|
|
||
| global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
|
|
||
| points_to_aes_key_st key_ptr user_key; | ||
|
|
||
| crucible_return (crucible_term {{ 0 : [32] }}); | ||
| }; | ||
|
|
||
|
|
||
| let aes_hw_encrypt_spec = do { | ||
| (in_, in_ptr) <- ptr_to_fresh_readonly "in" (llvm_array AES_BLOCK_SIZE (llvm_int 8)); | ||
| out_ptr <- crucible_alloc (llvm_array AES_BLOCK_SIZE (llvm_int 8)); | ||
| key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st"); | ||
| key <- fresh_aes_key_st; | ||
| points_to_aes_key_st key_ptr key; | ||
|
|
||
| crucible_execute_func [in_ptr, out_ptr, key_ptr]; | ||
|
|
||
| crucible_points_to out_ptr (crucible_term {{ aes_hw_encrypt in_ key }}); | ||
| }; | ||
|
|
||
| let aes_hw_encrypt_in_place_spec = do { | ||
| (in_, inout_ptr) <- ptr_to_fresh "in" (llvm_array AES_BLOCK_SIZE (llvm_int 8)); | ||
| key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st"); | ||
| key <- fresh_aes_key_st; | ||
| points_to_aes_key_st key_ptr key; | ||
|
|
||
| crucible_execute_func [inout_ptr, inout_ptr, key_ptr]; | ||
|
|
||
| crucible_points_to inout_ptr (crucible_term {{ aes_hw_encrypt in_ key }}); | ||
| }; | ||
|
|
||
|
|
||
| let aes_hw_decrypt_spec = do { | ||
| (in_, in_ptr) <- ptr_to_fresh_readonly "in" (llvm_array AES_BLOCK_SIZE (llvm_int 8)); | ||
| out_ptr <- crucible_alloc (llvm_array AES_BLOCK_SIZE (llvm_int 8)); | ||
| key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st"); | ||
| (key_low, key_high) <- fresh_aes_key_256_parts; | ||
| points_to_inv_aes_key_st key_ptr (key_low, key_high); | ||
|
|
||
| crucible_execute_func [in_ptr, out_ptr, key_ptr]; | ||
|
|
||
| crucible_points_to out_ptr (crucible_term {{ aes_hw_decrypt in_ (key_low # key_high) }}); | ||
| }; | ||
|
|
||
| let aes_hw_decrypt_in_place_spec = do { | ||
| (in_, inout_ptr) <- ptr_to_fresh "in" (llvm_array AES_BLOCK_SIZE (llvm_int 8)); | ||
| key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st"); | ||
| (key_low, key_high) <- fresh_aes_key_256_parts; | ||
| points_to_inv_aes_key_st key_ptr (key_low, key_high); | ||
|
|
||
| crucible_execute_func [inout_ptr, inout_ptr, key_ptr]; | ||
|
|
||
| crucible_points_to inout_ptr (crucible_term {{ aes_hw_decrypt in_ (key_low # key_high) }}); | ||
| }; | ||
|
|
||
|
|
||
| let aes_hw_ctr32_encrypt_blocks_spec len = do { | ||
| let len' = eval_size {| len * AES_BLOCK_SIZE |}; | ||
| global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
|
|
||
| (in_, in_ptr) <- ptr_to_fresh_readonly "in" (llvm_array len' (llvm_int 8)); | ||
| out_ptr <- crucible_alloc (llvm_array len' (llvm_int 8)); | ||
| key_ptr <- crucible_alloc_readonly (llvm_struct "struct.aes_key_st"); | ||
| key <- fresh_aes_key_st; | ||
| points_to_aes_key_st key_ptr key; | ||
| (ivec, ivec_ptr) <- ptr_to_fresh_readonly "ivec" (llvm_array AES_BLOCK_SIZE (llvm_int 8)); | ||
|
|
||
| crucible_execute_func [in_ptr, out_ptr, (crucible_term {{ `len : [64] }}), key_ptr, ivec_ptr]; | ||
|
|
||
| crucible_points_to out_ptr (crucible_term {{ aes_hw_ctr32_encrypt_blocks in_ key ivec }}); | ||
|
|
||
| global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }}; | ||
| }; | ||
|
|
||
|
|
||
|
|
||
| //////////////////////////////////////////////////////////////////////////////// | ||
| // Proof commands | ||
| aes_hw_set_encrypt_key_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aes_hw_set_encrypt_key" | ||
| [] | ||
| true | ||
| aes_hw_set_encrypt_key_spec | ||
| (do { | ||
| simplify (cryptol_ss ()); | ||
| simplify (addsimps slice_384_thms basic_ss); | ||
| w4_unint_yices ["SubByte'"]; | ||
| }); | ||
|
|
||
| aes_hw_encrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aes_hw_encrypt" | ||
| [] | ||
| true | ||
| aes_hw_encrypt_spec | ||
| (do { | ||
| simplify (cryptol_ss ()); | ||
| simplify (addsimps slice_384_thms basic_ss); | ||
| w4_unint_yices ["AESRound", "AESFinalRound"]; | ||
| }); | ||
| aes_hw_encrypt_in_place_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aes_hw_encrypt" | ||
| [] | ||
| true | ||
| aes_hw_encrypt_in_place_spec | ||
| (do { | ||
| simplify (cryptol_ss ()); | ||
| simplify (addsimps slice_384_thms basic_ss); | ||
| w4_unint_yices ["AESRound", "AESFinalRound"]; | ||
| }); | ||
|
|
||
| aes_hw_decrypt_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aes_hw_decrypt" | ||
| [] | ||
| true | ||
| aes_hw_decrypt_spec | ||
| (do { | ||
| simplify (cryptol_ss ()); | ||
| simplify (addsimps slice_384_thms basic_ss); | ||
| w4_unint_yices ["AESInvRound", "AESFinalInvRound"]; | ||
| }); | ||
| aes_hw_decrypt_in_place_ov <- llvm_verify_x86 m "../../build/x86/crypto/crypto_test" "aes_hw_decrypt" | ||
| [] | ||
| true | ||
| aes_hw_decrypt_in_place_spec | ||
| (do { | ||
| simplify (cryptol_ss ()); | ||
| simplify (addsimps slice_384_thms basic_ss); | ||
| w4_unint_yices ["AESInvRound", "AESFinalInvRound"]; | ||
| }); | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,156 @@ | ||
| /* | ||
| * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
| * SPDX-License-Identifier: Apache-2.0 | ||
| */ | ||
|
|
||
| /* | ||
| * Rewrite rules proofs and goal tactics. This does not | ||
| * contain any specifications or assumtions, thus it does | ||
| * not require inspection in order to trust the | ||
| * verification result. | ||
| */ | ||
|
|
||
| let slice_0_64_64 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 0 64 64 x"; | ||
| let slice_64_64_0 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 64 64 0 x"; | ||
| let slice_0_128_128 = parse_core "\\(x : Vec 256 Bool) -> slice Bool 0 128 128 x"; | ||
| let slice_128_128_0 = parse_core "\\(x : Vec 256 Bool) -> slice Bool 128 128 0 x"; | ||
| let slice_0_64_192 = parse_core "\\(x : Vec 256 Bool) -> slice Bool 0 64 192 x"; | ||
| let slice_64_64_128 = parse_core "\\(x : Vec 256 Bool) -> slice Bool 64 64 128 x"; | ||
| let slice_128_64_64 = parse_core "\\(x : Vec 256 Bool) -> slice Bool 128 64 64 x"; | ||
| let slice_192_64_0 = parse_core "\\(x : Vec 256 Bool) -> slice Bool 192 64 0 x"; | ||
| let slice_0_32_96 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 0 32 96 x"; | ||
| let slice_32_32_64 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 32 32 64 x"; | ||
| let slice_64_32_32 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 64 32 32 x"; | ||
| let slice_96_32_0 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 96 32 0 x"; | ||
| let slice_0_8_120 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 0 8 120 x"; | ||
| let slice_8_8_112 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 8 8 112 x"; | ||
| let slice_16_8_104 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 16 8 104 x"; | ||
| let slice_24_8_96 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 24 8 96 x"; | ||
| let slice_32_8_88 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 32 8 88 x"; | ||
| let slice_40_8_80 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 40 8 80 x"; | ||
| let slice_48_8_72 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 48 8 72 x"; | ||
| let slice_56_8_64 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 56 8 64 x"; | ||
| let slice_64_8_56 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 64 8 56 x"; | ||
| let slice_72_8_48 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 72 8 48 x"; | ||
| let slice_80_8_40 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 80 8 40 x"; | ||
| let slice_88_8_32 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 88 8 32 x"; | ||
| let slice_96_8_24 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 96 8 24 x"; | ||
| let slice_104_8_16 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 104 8 16 x"; | ||
| let slice_112_8_8 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 112 8 8 x"; | ||
| let slice_120_8_0 = parse_core "\\(x : Vec 128 Bool) -> slice Bool 120 8 0 x"; | ||
| let slice_0_8_56 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 0 8 56 x"; | ||
| let slice_8_8_48 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 8 8 48 x"; | ||
| let slice_16_8_40 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 16 8 40 x"; | ||
| let slice_24_8_32 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 24 8 32 x"; | ||
| let slice_32_8_24 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 32 8 24 x"; | ||
| let slice_40_8_16 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 40 8 16 x"; | ||
| let slice_48_8_8 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 48 8 8 x"; | ||
| let slice_56_8_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 56 8 0 x"; | ||
| let slice_384_128_0 = parse_core "\\(x : Vec 512 Bool) -> slice Bool 384 128 0 x"; | ||
| let slice_384_32_96 = parse_core "\\(x : Vec 512 Bool) -> slice Bool 384 32 96 x"; | ||
| let slice_416_32_64 = parse_core "\\(x : Vec 512 Bool) -> slice Bool 416 32 64 x"; | ||
| let slice_448_32_32 = parse_core "\\(x : Vec 512 Bool) -> slice Bool 448 32 32 x"; | ||
| let slice_480_32_0 = parse_core "\\(x : Vec 512 Bool) -> slice Bool 480 32 0 x"; | ||
| let slice_0_8_24 = parse_core "\\(x : Vec 32 Bool) -> slice Bool 0 8 24 x"; | ||
| let slice_8_8_16 = parse_core "\\(x : Vec 32 Bool) -> slice Bool 8 8 16 x"; | ||
| let slice_16_8_8 = parse_core "\\(x : Vec 32 Bool) -> slice Bool 16 8 8 x"; | ||
| let slice_24_8_0 = parse_core "\\(x : Vec 32 Bool) -> slice Bool 24 8 0 x"; | ||
| let slice_32_32_0 = parse_core "\\(x : Vec 64 Bool) -> slice Bool 32 32 0 x"; | ||
|
|
||
| let bvUExt_384_128 = parse_core "\\(x : Vec 128 Bool) -> bvUExt 384 128 x"; | ||
|
|
||
|
|
||
| slice_384_0_thm <- prove_folding_theorem {{ \x y -> slice_384_128_0 (x && y) == (slice_384_128_0 x) && (slice_384_128_0 y) }}; | ||
| slice_384_1_thm <- prove_folding_theorem {{ \x y -> slice_384_128_0 (x || y) == (slice_384_128_0 x) || (slice_384_128_0 y) }}; | ||
| slice_384_2_thm <- prove_folding_theorem {{ \x y -> slice_384_128_0 (x ^ y) == (slice_384_128_0 x) ^ (slice_384_128_0 y) }}; | ||
| slice_384_3_thm <- prove_folding_theorem {{ \x -> slice_384_128_0 (bvUExt_384_128 x) == x }}; | ||
| slice_384_4_thm <- prove_folding_theorem {{ \x -> slice_384_32_96 x == slice_0_32_96 (slice_384_128_0 x) }}; | ||
| slice_384_5_thm <- prove_folding_theorem {{ \x -> slice_416_32_64 x == slice_32_32_64 (slice_384_128_0 x) }}; | ||
| slice_384_6_thm <- prove_folding_theorem {{ \x -> slice_448_32_32 x == slice_64_32_32 (slice_384_128_0 x) }}; | ||
| slice_384_7_thm <- prove_folding_theorem {{ \x -> slice_480_32_0 x == slice_96_32_0 (slice_384_128_0 x) }}; | ||
| let slice_384_thms = | ||
| [ slice_384_0_thm | ||
| , slice_384_1_thm | ||
| , slice_384_2_thm | ||
| , slice_384_3_thm | ||
| , slice_384_4_thm | ||
| , slice_384_5_thm | ||
| , slice_384_6_thm | ||
| , slice_384_7_thm | ||
| ]; | ||
|
|
||
| slice_xor_8_thm <- prove_folding_theorem {{ \x y -> slice_0_8_24 (x ^ y) == (slice_0_8_24 x) ^ (slice_0_8_24 y) }}; | ||
| slice_xor_9_thm <- prove_folding_theorem {{ \x y -> slice_8_8_16 (x ^ y) == (slice_8_8_16 x) ^ (slice_8_8_16 y) }}; | ||
| slice_xor_10_thm <- prove_folding_theorem {{ \x y -> slice_16_8_8 (x ^ y) == (slice_16_8_8 x) ^ (slice_16_8_8 y) }}; | ||
| slice_xor_11_thm <- prove_folding_theorem {{ \x y -> slice_24_8_0 (x ^ y) == (slice_24_8_0 x) ^ (slice_24_8_0 y) }}; | ||
| slice_xor_12_thm <- prove_folding_theorem {{ \x y -> slice_0_8_120 (x ^ y) == (slice_0_8_120 x) ^ (slice_0_8_120 y) }}; | ||
| slice_xor_13_thm <- prove_folding_theorem {{ \x y -> slice_8_8_112 (x ^ y) == (slice_8_8_112 x) ^ (slice_8_8_112 y) }}; | ||
| slice_xor_14_thm <- prove_folding_theorem {{ \x y -> slice_16_8_104 (x ^ y) == (slice_16_8_104 x) ^ (slice_16_8_104 y) }}; | ||
| slice_xor_15_thm <- prove_folding_theorem {{ \x y -> slice_24_8_96 (x ^ y) == (slice_24_8_96 x) ^ (slice_24_8_96 y) }}; | ||
| slice_xor_16_thm <- prove_folding_theorem {{ \x y -> slice_32_8_88 (x ^ y) == (slice_32_8_88 x) ^ (slice_32_8_88 y) }}; | ||
| slice_xor_17_thm <- prove_folding_theorem {{ \x y -> slice_40_8_80 (x ^ y) == (slice_40_8_80 x) ^ (slice_40_8_80 y) }}; | ||
| slice_xor_18_thm <- prove_folding_theorem {{ \x y -> slice_48_8_72 (x ^ y) == (slice_48_8_72 x) ^ (slice_48_8_72 y) }}; | ||
| slice_xor_19_thm <- prove_folding_theorem {{ \x y -> slice_56_8_64 (x ^ y) == (slice_56_8_64 x) ^ (slice_56_8_64 y) }}; | ||
| slice_xor_20_thm <- prove_folding_theorem {{ \x y -> slice_64_8_56 (x ^ y) == (slice_64_8_56 x) ^ (slice_64_8_56 y) }}; | ||
| slice_xor_21_thm <- prove_folding_theorem {{ \x y -> slice_72_8_48 (x ^ y) == (slice_72_8_48 x) ^ (slice_72_8_48 y) }}; | ||
| slice_xor_22_thm <- prove_folding_theorem {{ \x y -> slice_80_8_40 (x ^ y) == (slice_80_8_40 x) ^ (slice_80_8_40 y) }}; | ||
| slice_xor_23_thm <- prove_folding_theorem {{ \x y -> slice_88_8_32 (x ^ y) == (slice_88_8_32 x) ^ (slice_88_8_32 y) }}; | ||
| slice_xor_24_thm <- prove_folding_theorem {{ \x y -> slice_96_8_24 (x ^ y) == (slice_96_8_24 x) ^ (slice_96_8_24 y) }}; | ||
| slice_xor_25_thm <- prove_folding_theorem {{ \x y -> slice_104_8_16 (x ^ y) == (slice_104_8_16 x) ^ (slice_104_8_16 y) }}; | ||
| slice_xor_26_thm <- prove_folding_theorem {{ \x y -> slice_112_8_8 (x ^ y) == (slice_112_8_8 x) ^ (slice_112_8_8 y) }}; | ||
| slice_xor_27_thm <- prove_folding_theorem {{ \x y -> slice_120_8_0 (x ^ y) == (slice_120_8_0 x) ^ (slice_120_8_0 y) }}; | ||
|
|
||
| slice_add_0_thm <- prove_folding_theorem {{ \x y -> slice_56_8_0 (x + y) == slice_24_8_0 ((slice_32_32_0 x) + (slice_32_32_0 y)) }}; | ||
| slice_add_1_thm <- prove_folding_theorem {{ \x y -> slice_48_8_8 (x + y) == slice_16_8_8 ((slice_32_32_0 x) + (slice_32_32_0 y)) }}; | ||
| slice_add_2_thm <- prove_folding_theorem {{ \x y -> slice_40_8_16 (x + y) == slice_8_8_16 ((slice_32_32_0 x) + (slice_32_32_0 y)) }}; | ||
| slice_add_3_thm <- prove_folding_theorem {{ \x y -> slice_32_8_24 (x + y) == slice_0_8_24 ((slice_32_32_0 x) + (slice_32_32_0 y)) }}; | ||
|
|
||
| let add_xor_slice_thms = | ||
| [ slice_add_0_thm | ||
| , slice_add_1_thm | ||
| , slice_add_2_thm | ||
| , slice_add_3_thm | ||
| , slice_xor_8_thm | ||
| , slice_xor_9_thm | ||
| , slice_xor_10_thm | ||
| , slice_xor_11_thm | ||
| , slice_xor_12_thm | ||
| , slice_xor_13_thm | ||
| , slice_xor_14_thm | ||
| , slice_xor_15_thm | ||
| , slice_xor_16_thm | ||
| , slice_xor_17_thm | ||
| , slice_xor_18_thm | ||
| , slice_xor_19_thm | ||
| , slice_xor_20_thm | ||
| , slice_xor_21_thm | ||
| , slice_xor_22_thm | ||
| , slice_xor_23_thm | ||
| , slice_xor_24_thm | ||
| , slice_xor_25_thm | ||
| , slice_xor_26_thm | ||
| , slice_xor_27_thm | ||
| ]; | ||
|
|
||
| aesenclast_0_thm <- prove_print | ||
| (do { | ||
| w4_unint_yices ["ShiftRows", "SubBytes"]; | ||
| }) | ||
| (rewrite (cryptol_ss ()) {{ \(x : [8]) y z key -> aesenclast key ((x # y) ^ z) == (x # y) ^ (aesenclast key z) }}); | ||
| aesenclast_1_thm <- prove_print | ||
| (do { | ||
| w4_unint_yices ["ShiftRows", "SubBytes"]; | ||
| }) | ||
| (rewrite (cryptol_ss ()) {{ \(x : [8]) y z key -> aesenclast key (z ^ (x # y)) == (x # y) ^ (aesenclast key z) }}); | ||
| let aesenclast_thms = | ||
| [ aesenclast_0_thm | ||
| , aesenclast_1_thm | ||
| ]; | ||
|
|
||
| // replace (bvult x y) with (x - y <$ 0) in order for the semiring and abstract | ||
| // domain to work. This simplifies goals related to the 64-byte alignment of | ||
| // the stack. | ||
| let bvult = parse_core "\\(x y : Vec 64 Bool) -> bvult 64 x y"; | ||
| cmp_sub_thm <- prove_folding_theorem | ||
| {{ \x y -> bvult x y == if (x @ 0 == y @ 0) then (x - y <$ 0) else (x @ 0 < y @ 0) }}; | ||
|
|
Oops, something went wrong.