From 84ada38e4caa384f2676352239c20e2111062379 Mon Sep 17 00:00:00 2001 From: sanketh Date: Thu, 12 Mar 2026 21:43:43 +0000 Subject: [PATCH 1/7] Add FIPS 197 AES cipher specification with KATs Add HOL Light definitions for AES-128 and AES-256 following NIST FIPS 197 exactly, independent from the hardware-oriented model in common/aes.ml. Uses NIST ordering (SubBytes before ShiftRows) throughout. New files: - common/fips197.ml: key expansion, cipher steps, full cipher, and KATs - {arm,x86}/proofs/fips197.ml: loaders for standard build-proof.sh validation Definitions: aes128_kexp_round, aes256_kexp_round, aes256_kexp_last, fips197_sub_bytes, fips197_shift_rows, fips197_mix_columns, fips197_add_round_key, fips197_round, fips197_final_round, aes128_cipher, aes256_cipher. KATs: FIPS 197 Appendices A.1, A.3, B; NIST AES_Core256; AESAVS GFSbox. To validate: cd x86 && make proofs/fips197.correct or: cd arm && make proofs/fips197.correct --- arm/proofs/fips197.ml | 9 + common/fips197.ml | 514 ++++++++++++++++++++++++++++++++++++++++++ x86/proofs/fips197.ml | 9 + 3 files changed, 532 insertions(+) create mode 100644 arm/proofs/fips197.ml create mode 100644 common/fips197.ml create mode 100644 x86/proofs/fips197.ml diff --git a/arm/proofs/fips197.ml b/arm/proofs/fips197.ml new file mode 100644 index 000000000..baa13d1a8 --- /dev/null +++ b/arm/proofs/fips197.ml @@ -0,0 +1,9 @@ +(* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0 + *) + +(* Load and validate common/fips197.ml definitions and KATs. *) + +needs "arm/proofs/base.ml";; +needs "common/fips197.ml";; diff --git a/common/fips197.ml b/common/fips197.ml new file mode 100644 index 000000000..b279bc2de --- /dev/null +++ b/common/fips197.ml @@ -0,0 +1,514 @@ +(* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0 + *) + +(* ========================================================================= *) +(* AES definitions per FIPS 197. *) +(* *) +(* This file defines AES key expansion and cipher following the NIST spec *) +(* exactly (SubBytes before ShiftRows). It is independent from the *) +(* hardware-oriented definitions in common/aes.ml and arm/x86 proofs. *) +(* Equivalence can be proved separately. *) +(* *) +(* Key expansion reuses aes_subword from common/aes.ml (SubWord is the *) +(* same in both NIST and hardware models). *) +(* ========================================================================= *) + +needs "common/aes.ml";; + +(* ========================================================================= *) +(* AES Key Expansion (FIPS 197 Sec 5.2) *) +(* ========================================================================= *) + +(* Key expansion core step (FIPS 197 Sec 5.2): + w[i] = w[i-Nk] XOR SubWord(RotWord(w[i-1])) XOR Rcon[i/Nk] *) +let aes_kexp_core = new_definition + `aes_kexp_core (rcon:32 word) (prev:32 word) (back:32 word) : 32 word = + word_xor back (word_xor (aes_subword (word_rol prev 8)) rcon)`;; + +let AES_KEXP_CORE_CONV = + REWRITE_CONV [aes_kexp_core] THENC + AES_SUBWORD_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +(* SubWord-only step (FIPS 197 Sec 5.2: when Nk>6 and i mod Nk = 4) *) +let aes_kexp_sub = new_definition + `aes_kexp_sub (prev:32 word) (back:32 word) : 32 word = + word_xor back (aes_subword prev)`;; + +let AES_KEXP_SUB_CONV = + REWRITE_CONV [aes_kexp_sub] THENC + AES_SUBWORD_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +(* Round constants (FIPS 197 Table 5) *) +let aes_rcon = new_definition + `aes_rcon : (32 word) list = + [ word 0x01000000; word 0x02000000; word 0x04000000; word 0x08000000 + ; word 0x10000000; word 0x20000000; word 0x40000000; word 0x80000000 + ; word 0x1b000000; word 0x36000000 ]`;; + +(* Pre-computed EL reductions for 10-element 32-bit word lists. *) +let EL_10_32_CLAUSES = + let pat = `EL n [x0;x1;x2;x3;x4;x5;x6;x7;x8;x9]:32 word` in + map (fun n -> EL_CONV(subst [mk_small_numeral n,`n:num`] pat)) (0--9);; + +(* AES-128 key expansion round (FIPS 197 Sec 5.2, Nk=4). *) +let aes128_kexp_round = new_definition + `aes128_kexp_round (i:num) + (w0:32 word, w1:32 word, w2:32 word, w3:32 word) + : 32 word # 32 word # 32 word # 32 word = + let w4 = aes_kexp_core (EL i aes_rcon) w3 w0 in + let w5 = word_xor w1 w4 in + let w6 = word_xor w2 w5 in + let w7 = word_xor w3 w6 in + (w4, w5, w6, w7)`;; + +(* Conversion for aes128_kexp_round. *) +let AES128_KEXP_ROUND_CONV = + REWRITE_CONV [aes128_kexp_round; aes_rcon] THENC + REWRITE_CONV EL_10_32_CLAUSES THENC + TOP_DEPTH_CONV let_CONV THENC + AES_KEXP_CORE_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +(* AES-256 key expansion round (FIPS 197 Sec 5.2, Nk=8 case). + Given round index i (0-6) and the previous 8 words, produce the next 8. *) +let aes256_kexp_round = new_definition + `aes256_kexp_round (i:num) + (w0:32 word, w1:32 word, w2:32 word, w3:32 word, + w4:32 word, w5:32 word, w6:32 word, w7:32 word) + : 32 word # 32 word # 32 word # 32 word # + 32 word # 32 word # 32 word # 32 word = + let w8 = aes_kexp_core (EL i aes_rcon) w7 w0 in + let w9 = word_xor w1 w8 in + let w10 = word_xor w2 w9 in + let w11 = word_xor w3 w10 in + let w12 = aes_kexp_sub w11 w4 in + let w13 = word_xor w5 w12 in + let w14 = word_xor w6 w13 in + let w15 = word_xor w7 w14 in + (w8, w9, w10, w11, w12, w13, w14, w15)`;; + +let AES256_KEXP_ROUND_CONV = + REWRITE_CONV [aes256_kexp_round; aes_rcon] THENC + REWRITE_CONV EL_10_32_CLAUSES THENC + TOP_DEPTH_CONV let_CONV THENC + AES_KEXP_CORE_CONV THENC + AES_KEXP_SUB_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +(* AES-256 last half-round: only 4 words (core step, no SubWord step). *) +let aes256_kexp_last = new_definition + `aes256_kexp_last (i:num) + (w0:32 word, w1:32 word, w2:32 word, w3:32 word, + w4:32 word, w5:32 word, w6:32 word, w7:32 word) + : 32 word # 32 word # 32 word # 32 word = + let w8 = aes_kexp_core (EL i aes_rcon) w7 w0 in + let w9 = word_xor w1 w8 in + let w10 = word_xor w2 w9 in + let w11 = word_xor w3 w10 in + (w8, w9, w10, w11)`;; + +let AES256_KEXP_LAST_CONV = + REWRITE_CONV [aes256_kexp_last; aes_rcon] THENC + REWRITE_CONV EL_10_32_CLAUSES THENC + TOP_DEPTH_CONV let_CONV THENC + AES_KEXP_CORE_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +(* ========================================================================= *) +(* KAT: AES-128 Key Expansion (FIPS 197 Appendix A.1) *) +(* Key = 2b7e1516 28aed2a6 abf71588 09cf4f3c *) +(* ========================================================================= *) + +prove(`aes128_kexp_round 0 + (word 0x2b7e1516, word 0x28aed2a6, word 0xabf71588, word 0x09cf4f3c) = + (word 0xa0fafe17, word 0x88542cb1, word 0x23a33939, word 0x2a6c7605)`, + CONV_TAC(LAND_CONV AES128_KEXP_ROUND_CONV) THEN REFL_TAC);; + +prove(`aes128_kexp_round 9 + (aes128_kexp_round 8 + (aes128_kexp_round 7 + (aes128_kexp_round 6 + (aes128_kexp_round 5 + (aes128_kexp_round 4 + (aes128_kexp_round 3 + (aes128_kexp_round 2 + (aes128_kexp_round 1 + (aes128_kexp_round 0 + (word 0x2b7e1516, word 0x28aed2a6, + word 0xabf71588, word 0x09cf4f3c)))))))))) = + (word 0xd014f9a8, word 0xc9ee2589, word 0xe13f0cc8, word 0xb6630ca6)`, + CONV_TAC(LAND_CONV( + RAND_CONV(RAND_CONV(RAND_CONV(RAND_CONV(RAND_CONV(RAND_CONV( + RAND_CONV(RAND_CONV(RAND_CONV AES128_KEXP_ROUND_CONV THENC + AES128_KEXP_ROUND_CONV) THENC + AES128_KEXP_ROUND_CONV) THENC + AES128_KEXP_ROUND_CONV) THENC + AES128_KEXP_ROUND_CONV) THENC + AES128_KEXP_ROUND_CONV) THENC + AES128_KEXP_ROUND_CONV) THENC + AES128_KEXP_ROUND_CONV) THENC + AES128_KEXP_ROUND_CONV) THENC + AES128_KEXP_ROUND_CONV)) THEN + REFL_TAC);; + +(* ========================================================================= *) +(* KAT: AES-256 Key Expansion (FIPS 197 Appendix A.3) *) +(* Key = 603deb10 15ca71be 2b73aef0 857d7781 *) +(* 1f352c07 3b6108d7 2d9810a3 0914dff4 *) +(* ========================================================================= *) + +prove(`aes256_kexp_round 0 + (word 0x603deb10, word 0x15ca71be, word 0x2b73aef0, word 0x857d7781, + word 0x1f352c07, word 0x3b6108d7, word 0x2d9810a3, word 0x0914dff4) = + (word 0x9ba35411, word 0x8e6925af, word 0xa51a8b5f, word 0x2067fcde, + word 0xa8b09c1a, word 0x93d194cd, word 0xbe49846e, word 0xb75d5b9a)`, + CONV_TAC(LAND_CONV AES256_KEXP_ROUND_CONV) THEN REFL_TAC);; + +prove(`aes256_kexp_last 6 + (aes256_kexp_round 5 + (aes256_kexp_round 4 + (aes256_kexp_round 3 + (aes256_kexp_round 2 + (aes256_kexp_round 1 + (aes256_kexp_round 0 + (word 0x603deb10, word 0x15ca71be, + word 0x2b73aef0, word 0x857d7781, + word 0x1f352c07, word 0x3b6108d7, + word 0x2d9810a3, word 0x0914dff4))))))) = + (word 0xfe4890d1, word 0xe6188d0b, word 0x046df344, word 0x706c631e)`, + CONV_TAC(LAND_CONV( + RAND_CONV(RAND_CONV(RAND_CONV(RAND_CONV(RAND_CONV( + RAND_CONV AES256_KEXP_ROUND_CONV THENC + AES256_KEXP_ROUND_CONV) THENC + AES256_KEXP_ROUND_CONV) THENC + AES256_KEXP_ROUND_CONV) THENC + AES256_KEXP_ROUND_CONV) THENC + AES256_KEXP_ROUND_CONV) THENC + AES256_KEXP_LAST_CONV)) THEN + REFL_TAC);; + +(* ========================================================================= *) +(* AES Cipher steps (FIPS 197 Sec 5.1) *) +(* NIST byte ordering: byte 0 = MSB of 128-bit word. *) +(* NIST round order: SubBytes -> ShiftRows -> MixColumns -> AddRoundKey. *) +(* ========================================================================= *) + +(* SubBytes: apply S-box to each byte. *) +let fips197_sub_bytes = new_definition + `fips197_sub_bytes (s:128 word) : 128 word = + aes_sub_bytes joined_GF2 s`;; + +(* ShiftRows (FIPS 197 Sec 5.1.2): s'[r,c] = s[r, (c+r) mod 4]. *) +let fips197_shift_rows = new_definition + `fips197_shift_rows (op:128 word) : 128 word = + word_join_list_16_8 + [ (word_subword op (120, 8)) + ; (word_subword op (80, 8)) + ; (word_subword op (40, 8)) + ; (word_subword op (0, 8)) + ; (word_subword op (88, 8)) + ; (word_subword op (48, 8)) + ; (word_subword op (8, 8)) + ; (word_subword op (96, 8)) + ; (word_subword op (56, 8)) + ; (word_subword op (16, 8)) + ; (word_subword op (104, 8)) + ; (word_subword op (64, 8)) + ; (word_subword op (24, 8)) + ; (word_subword op (112, 8)) + ; (word_subword op (72, 8)) + ; (word_subword op (32, 8)) ]`;; + +let FIPS197_SUB_BYTES_CONV = + REWRITE_CONV [fips197_sub_bytes] THENC AES_SUB_BYTES_CONV;; + +let FIPS197_SHIFT_ROWS_CONV = + REWRITE_CONV [fips197_shift_rows] THENC + WORD_JOIN_LIST_16_8_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +(* KAT: FIPS 197 Appendix B, Round 1 SubBytes *) +prove(`fips197_sub_bytes (word 0x193de3bea0f4e22b9ac68d2ae9f84808) = + word 0xd42711aee0bf98f1b8b45de51e415230`, + CONV_TAC(LAND_CONV FIPS197_SUB_BYTES_CONV) THEN REFL_TAC);; + +(* KAT: FIPS 197 Appendix B, Round 1 ShiftRows *) +prove(`fips197_shift_rows (word 0xd42711aee0bf98f1b8b45de51e415230) = + word 0xd4bf5d30e0b452aeb84111f11e2798e5`, + CONV_TAC(LAND_CONV FIPS197_SHIFT_ROWS_CONV) THEN REFL_TAC);; + +(* MixColumns (FIPS 197 Sec 5.1.3). *) +let fips197_mix_columns = new_definition + `fips197_mix_columns (op:128 word) : 128 word = + let d00 = aes_mix_word op 120 112 104 96 in + let d10 = aes_mix_word op 112 104 96 120 in + let d20 = aes_mix_word op 104 96 120 112 in + let d30 = aes_mix_word op 96 120 112 104 in + let d01 = aes_mix_word op 88 80 72 64 in + let d11 = aes_mix_word op 80 72 64 88 in + let d21 = aes_mix_word op 72 64 88 80 in + let d31 = aes_mix_word op 64 88 80 72 in + let d02 = aes_mix_word op 56 48 40 32 in + let d12 = aes_mix_word op 48 40 32 56 in + let d22 = aes_mix_word op 40 32 56 48 in + let d32 = aes_mix_word op 32 56 48 40 in + let d03 = aes_mix_word op 24 16 8 0 in + let d13 = aes_mix_word op 16 8 0 24 in + let d23 = aes_mix_word op 8 0 24 16 in + let d33 = aes_mix_word op 0 24 16 8 in + word_join_list_16_8 + [d00; d10; d20; d30; d01; d11; d21; d31; + d02; d12; d22; d32; d03; d13; d23; d33]`;; + +let FIPS197_MIX_COLUMNS_CONV = + REWRITE_CONV [fips197_mix_columns] THENC + AES_MIX_WORD_CONV THENC + WORD_JOIN_LIST_16_8_CONV THENC + TOP_DEPTH_CONV let_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +(* KAT: FIPS 197 Appendix B, Round 1 MixColumns *) +prove(`fips197_mix_columns (word 0xd4bf5d30e0b452aeb84111f11e2798e5) = + word 0x046681e5e0cb199a48f8d37a2806264c`, + CONV_TAC(LAND_CONV FIPS197_MIX_COLUMNS_CONV) THEN REFL_TAC);; + +(* ========================================================================= *) +(* AddRoundKey (FIPS 197 Sec 5.1.4): XOR state with round key. *) +(* ========================================================================= *) + +let fips197_add_round_key = new_definition + `fips197_add_round_key (s:128 word) (k:128 word) : 128 word = word_xor s k`;; + +(* KAT: FIPS 197 Appendix B, Round 1 AddRoundKey *) +prove(`fips197_add_round_key (word 0x046681e5e0cb199a48f8d37a2806264c) + (word 0xa0fafe1788542cb123a339392a6c7605) = + word 0xa49c7ff2689f352b6b5bea43026a5049`, + CONV_TAC(REWRITE_CONV [fips197_add_round_key] THENC + DEPTH_CONV WORD_RED_CONV) THEN REFL_TAC);; + +(* ========================================================================= *) +(* AES Cipher (FIPS 197 Algorithm 1) — unrolled *) +(* ========================================================================= *) + +let fips197_round = new_definition + `fips197_round (state:128 word) (round_key:128 word) : 128 word = + word_xor + (fips197_mix_columns (fips197_shift_rows (fips197_sub_bytes state))) + round_key`;; + +let fips197_final_round = new_definition + `fips197_final_round (state:128 word) (round_key:128 word) : 128 word = + word_xor + (fips197_shift_rows (fips197_sub_bytes state)) + round_key`;; + +(* AES-128: 10 rounds (1 initial AddRoundKey + 9 middle + 1 final) *) +let aes128_cipher = new_definition + `aes128_cipher (plaintext:128 word) (ks:(128 word) list) : 128 word = + let s0 = word_xor plaintext (EL 0 ks) in + let s1 = fips197_round s0 (EL 1 ks) in + let s2 = fips197_round s1 (EL 2 ks) in + let s3 = fips197_round s2 (EL 3 ks) in + let s4 = fips197_round s3 (EL 4 ks) in + let s5 = fips197_round s4 (EL 5 ks) in + let s6 = fips197_round s5 (EL 6 ks) in + let s7 = fips197_round s6 (EL 7 ks) in + let s8 = fips197_round s7 (EL 8 ks) in + let s9 = fips197_round s8 (EL 9 ks) in + fips197_final_round s9 (EL 10 ks)`;; + +(* AES-256: 14 rounds (1 initial AddRoundKey + 13 middle + 1 final) *) +let aes256_cipher = new_definition + `aes256_cipher (plaintext:128 word) (ks:(128 word) list) : 128 word = + let s0 = word_xor plaintext (EL 0 ks) in + let s1 = fips197_round s0 (EL 1 ks) in + let s2 = fips197_round s1 (EL 2 ks) in + let s3 = fips197_round s2 (EL 3 ks) in + let s4 = fips197_round s3 (EL 4 ks) in + let s5 = fips197_round s4 (EL 5 ks) in + let s6 = fips197_round s5 (EL 6 ks) in + let s7 = fips197_round s6 (EL 7 ks) in + let s8 = fips197_round s7 (EL 8 ks) in + let s9 = fips197_round s8 (EL 9 ks) in + let s10 = fips197_round s9 (EL 10 ks) in + let s11 = fips197_round s10 (EL 11 ks) in + let s12 = fips197_round s11 (EL 12 ks) in + let s13 = fips197_round s12 (EL 13 ks) in + fips197_final_round s13 (EL 14 ks)`;; + +(* ========================================================================= *) +(* Conversions for evaluating the cipher on concrete inputs *) +(* ========================================================================= *) + +let FIPS197_ROUND_CONV = + REWRITE_CONV [fips197_round] THENC + FIPS197_SUB_BYTES_CONV THENC + FIPS197_SHIFT_ROWS_CONV THENC + FIPS197_MIX_COLUMNS_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +let FIPS197_ROUND_REDUCE_CONV tm = + match tm with + Comb(Comb(Const("fips197_round",_), + Comb(Const("word",_),s)), + Comb(Const("word",_),k)) + when is_numeral s && is_numeral k -> FIPS197_ROUND_CONV tm + | _ -> failwith "FIPS197_ROUND_REDUCE_CONV";; + +let FIPS197_FINAL_ROUND_CONV = + REWRITE_CONV [fips197_final_round] THENC + FIPS197_SUB_BYTES_CONV THENC + FIPS197_SHIFT_ROWS_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +let FIPS197_FINAL_ROUND_REDUCE_CONV tm = + match tm with + Comb(Comb(Const("fips197_final_round",_), + Comb(Const("word",_),s)), + Comb(Const("word",_),k)) + when is_numeral s && is_numeral k -> FIPS197_FINAL_ROUND_CONV tm + | _ -> failwith "FIPS197_FINAL_ROUND_REDUCE_CONV";; + +let FIPS197_ENCRYPT_CONV cipher_def ks_def = + REWRITE_CONV [ks_def] THENC + REWRITE_CONV [cipher_def] THENC + TOP_DEPTH_CONV let_CONV THENC + DEPTH_CONV (EL_CONV ORELSEC WORD_RED_CONV ORELSEC NUM_RED_CONV) THENC + DEPTH_CONV FIPS197_ROUND_REDUCE_CONV THENC + FIPS197_FINAL_ROUND_REDUCE_CONV;; + +(* ========================================================================= *) +(* KAT: FIPS 197 Appendix B — AES-128 full encryption *) +(* Plaintext: 0x3243f6a8885a308d313198a2e0370734 *) +(* Key: 0x2b7e151628aed2a6abf7158809cf4f3c *) +(* Ciphertext: 0x3925841d02dc09fbdc118597196a0b32 *) +(* ========================================================================= *) + +let AES128_APPENDIX_B_KEY_SCHEDULE = new_definition + `AES128_APPENDIX_B_KEY_SCHEDULE:(128 word) list = + [ word 0x2b7e151628aed2a6abf7158809cf4f3c + ; word 0xa0fafe1788542cb123a339392a6c7605 + ; word 0xf2c295f27a96b9435935807a7359f67f + ; word 0x3d80477d4716fe3e1e237e446d7a883b + ; word 0xef44a541a8525b7fb671253bdb0bad00 + ; word 0xd4d1c6f87c839d87caf2b8bc11f915bc + ; word 0x6d88a37a110b3efddbf98641ca0093fd + ; word 0x4e54f70e5f5fc9f384a64fb24ea6dc4f + ; word 0xead27321b58dbad2312bf5607f8d292f + ; word 0xac7766f319fadc2128d12941575c006e + ; word 0xd014f9a8c9ee2589e13f0cc8b6630ca6 + ]`;; + +prove(`aes128_cipher (word 0x3243f6a8885a308d313198a2e0370734) + AES128_APPENDIX_B_KEY_SCHEDULE = + word 0x3925841d02dc09fbdc118597196a0b32`, + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes128_cipher + AES128_APPENDIX_B_KEY_SCHEDULE)) THEN REFL_TAC);; + +(* ========================================================================= *) +(* KAT: AES-256 full encryption (NIST AES_Core256 / FIPS 197 Appendix A.3) *) +(* Key: 0x603deb1015ca71be2b73aef0857d7781 *) +(* 1f352c073b6108d72d9810a30914dff4 *) +(* Plaintext: 0x6bc1bee22e409f96e93d7e117393172a *) +(* Ciphertext: 0xf3eed1bdb5d2a03c064b5a7e3db181f8 *) +(* ========================================================================= *) + +let AES256_CORE_KEY_SCHEDULE = new_definition + `AES256_CORE_KEY_SCHEDULE:(128 word) list = + [ word 0x603DEB1015CA71BE2B73AEF0857D7781 + ; word 0x1F352C073B6108D72D9810A30914DFF4 + ; word 0x9BA354118E6925AFA51A8B5F2067FCDE + ; word 0xA8B09C1A93D194CDBE49846EB75D5B9A + ; word 0xD59AECB85BF3C917FEE94248DE8EBE96 + ; word 0xB5A9328A2678A647983122292F6C79B3 + ; word 0x812C81ADDADF48BA24360AF2FAB8B464 + ; word 0x98C5BFC9BEBD198E268C3BA709E04214 + ; word 0x68007BACB2DF331696E939E46C518D80 + ; word 0xC814E20476A9FB8A5025C02D59C58239 + ; word 0xDE1369676CCC5A71FA2563959674EE15 + ; word 0x5886CA5D2E2F31D77E0AF1FA27CF73C3 + ; word 0x749C47AB18501DDAE2757E4F7401905A + ; word 0xCAFAAAE3E4D59B349ADF6ACEBD10190D + ; word 0xFE4890D1E6188D0B046DF344706C631E + ]`;; + +prove(`aes256_cipher (word 0x6bc1bee22e409f96e93d7e117393172a) + AES256_CORE_KEY_SCHEDULE = + word 0xf3eed1bdb5d2a03c064b5a7e3db181f8`, + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes256_cipher + AES256_CORE_KEY_SCHEDULE)) THEN REFL_TAC);; + +(* ========================================================================= *) +(* KAT: AESAVS Appendix B GFSbox — AES-128 with all-zero key *) +(* Source: "The Advanced Encryption Standard Algorithm Validation Suite" *) +(* ========================================================================= *) + +let AESAVS_ZERO_KEY_128_SCHEDULE = new_definition + `AESAVS_ZERO_KEY_128_SCHEDULE:(128 word) list = + [ word 0x00000000000000000000000000000000 + ; word 0x62636363626363636263636362636363 + ; word 0x9B9898C9F9FBFBAA9B9898C9F9FBFBAA + ; word 0x90973450696CCFFAF2F457330B0FAC99 + ; word 0xEE06DA7B876A1581759E42B27E91EE2B + ; word 0x7F2E2B88F8443E098DDA7CBBF34B9290 + ; word 0xEC614B851425758C99FF09376AB49BA7 + ; word 0x217517873550620BACAF6B3CC61BF09B + ; word 0x0EF903333BA9613897060A04511DFA9F + ; word 0xB1D4D8E28A7DB9DA1D7BB3DE4C664941 + ; word 0xB4EF5BCB3E92E21123E951CF6F8F188E + ]`;; + +(* AESAVS GFSbox first vector: key=0, pt=f34481ec... *) +prove(`aes128_cipher (word 0xf34481ec3cc627bacd5dc3fb08f273e6) + AESAVS_ZERO_KEY_128_SCHEDULE = + word 0x0336763e966d92595a567cc9ce537f5e`, + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes128_cipher + AESAVS_ZERO_KEY_128_SCHEDULE)) THEN REFL_TAC);; + +(* AESAVS: key=0, pt=0 *) +prove(`aes128_cipher (word 0x00000000000000000000000000000000) + AESAVS_ZERO_KEY_128_SCHEDULE = + word 0x66e94bd4ef8a2c3b884cfa59ca342b2e`, + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes128_cipher + AESAVS_ZERO_KEY_128_SCHEDULE)) THEN REFL_TAC);; + +(* ========================================================================= *) +(* KAT: AES-256 with all-zero key *) +(* ========================================================================= *) + +let AESAVS_ZERO_KEY_256_SCHEDULE = new_definition + `AESAVS_ZERO_KEY_256_SCHEDULE:(128 word) list = + [ word 0x00000000000000000000000000000000 + ; word 0x00000000000000000000000000000000 + ; word 0x62636363626363636263636362636363 + ; word 0xAAFBFBFBAAFBFBFBAAFBFBFBAAFBFBFB + ; word 0x6F6C6CCF0D0F0FAC6F6C6CCF0D0F0FAC + ; word 0x7D8D8D6AD77676917D8D8D6AD7767691 + ; word 0x5354EDC15E5BE26D31378EA23C38810E + ; word 0x968A81C141FCF7503C717A3AEB070CAB + ; word 0x9EAA8F28C0F16D45F1C6E3E7CDFE62E9 + ; word 0x2B312BDF6ACDDC8F56BCA6B5BDBBAA1E + ; word 0x6406FD52A4F79017553173F098CF1119 + ; word 0x6DBBA90B0776758451CAD331EC71792F + ; word 0xE7B0E89C4347788B16760B7B8EB91A62 + ; word 0x74ED0BA1739B7E252251AD14CE20D43B + ; word 0x10F80A1753BF729C45C979E7CB706385 + ]`;; + +(* AES-256: key=0, pt=0 *) +prove(`aes256_cipher (word 0x00000000000000000000000000000000) + AESAVS_ZERO_KEY_256_SCHEDULE = + word 0xdc95c078a2408989ad48a21492842087`, + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes256_cipher + AESAVS_ZERO_KEY_256_SCHEDULE)) THEN REFL_TAC);; + +(* AESAVS GFSbox first vector: key=0, pt=014730f8... *) +prove(`aes256_cipher (word 0x014730f80ac625fe84f026c60bfd547d) + AESAVS_ZERO_KEY_256_SCHEDULE = + word 0x5c9d844ed46f9885085e5d6a4f94c7d7`, + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes256_cipher + AESAVS_ZERO_KEY_256_SCHEDULE)) THEN REFL_TAC);; diff --git a/x86/proofs/fips197.ml b/x86/proofs/fips197.ml new file mode 100644 index 000000000..53e1ec89a --- /dev/null +++ b/x86/proofs/fips197.ml @@ -0,0 +1,9 @@ +(* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0 + *) + +(* Load and validate common/fips197.ml definitions and KATs. *) + +needs "x86/proofs/base.ml";; +needs "common/fips197.ml";; From a8a5585a277e5f77ea7498cae49ee91ebf270770 Mon Sep 17 00:00:00 2001 From: sanketh Date: Thu, 19 Mar 2026 18:24:15 +0000 Subject: [PATCH 2/7] whitespace --- common/fips197.ml | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/common/fips197.ml b/common/fips197.ml index b279bc2de..c0cc867ac 100644 --- a/common/fips197.ml +++ b/common/fips197.ml @@ -119,8 +119,8 @@ let AES256_KEXP_LAST_CONV = DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; (* ========================================================================= *) -(* KAT: AES-128 Key Expansion (FIPS 197 Appendix A.1) *) -(* Key = 2b7e1516 28aed2a6 abf71588 09cf4f3c *) +(* KAT: AES-128 Key Expansion (FIPS 197 Appendix A.1) *) +(* Key = 2b7e1516 28aed2a6 abf71588 09cf4f3c *) (* ========================================================================= *) prove(`aes128_kexp_round 0 @@ -156,9 +156,9 @@ prove(`aes128_kexp_round 9 REFL_TAC);; (* ========================================================================= *) -(* KAT: AES-256 Key Expansion (FIPS 197 Appendix A.3) *) -(* Key = 603deb10 15ca71be 2b73aef0 857d7781 *) -(* 1f352c07 3b6108d7 2d9810a3 0914dff4 *) +(* KAT: AES-256 Key Expansion (FIPS 197 Appendix A.3) *) +(* Key = 603deb10 15ca71be 2b73aef0 857d7781 *) +(* 1f352c07 3b6108d7 2d9810a3 0914dff4 *) (* ========================================================================= *) prove(`aes256_kexp_round 0 @@ -192,8 +192,8 @@ prove(`aes256_kexp_last 6 REFL_TAC);; (* ========================================================================= *) -(* AES Cipher steps (FIPS 197 Sec 5.1) *) -(* NIST byte ordering: byte 0 = MSB of 128-bit word. *) +(* AES Cipher steps (FIPS 197 Sec 5.1) *) +(* NIST byte ordering: byte 0 = MSB of 128-bit word. *) (* NIST round order: SubBytes -> ShiftRows -> MixColumns -> AddRoundKey. *) (* ========================================================================= *) @@ -277,7 +277,7 @@ prove(`fips197_mix_columns (word 0xd4bf5d30e0b452aeb84111f11e2798e5) = CONV_TAC(LAND_CONV FIPS197_MIX_COLUMNS_CONV) THEN REFL_TAC);; (* ========================================================================= *) -(* AddRoundKey (FIPS 197 Sec 5.1.4): XOR state with round key. *) +(* AddRoundKey (FIPS 197 Sec 5.1.4): XOR state with round key. *) (* ========================================================================= *) let fips197_add_round_key = new_definition @@ -382,7 +382,7 @@ let FIPS197_ENCRYPT_CONV cipher_def ks_def = FIPS197_FINAL_ROUND_REDUCE_CONV;; (* ========================================================================= *) -(* KAT: FIPS 197 Appendix B — AES-128 full encryption *) +(* KAT: FIPS 197 Appendix B — AES-128 full encryption *) (* Plaintext: 0x3243f6a8885a308d313198a2e0370734 *) (* Key: 0x2b7e151628aed2a6abf7158809cf4f3c *) (* Ciphertext: 0x3925841d02dc09fbdc118597196a0b32 *) @@ -410,7 +410,7 @@ prove(`aes128_cipher (word 0x3243f6a8885a308d313198a2e0370734) AES128_APPENDIX_B_KEY_SCHEDULE)) THEN REFL_TAC);; (* ========================================================================= *) -(* KAT: AES-256 full encryption (NIST AES_Core256 / FIPS 197 Appendix A.3) *) +(* KAT: AES-256 full encryption (NIST AES_Core256 / FIPS 197 Appendix A.3) *) (* Key: 0x603deb1015ca71be2b73aef0857d7781 *) (* 1f352c073b6108d72d9810a30914dff4 *) (* Plaintext: 0x6bc1bee22e409f96e93d7e117393172a *) @@ -443,8 +443,8 @@ prove(`aes256_cipher (word 0x6bc1bee22e409f96e93d7e117393172a) AES256_CORE_KEY_SCHEDULE)) THEN REFL_TAC);; (* ========================================================================= *) -(* KAT: AESAVS Appendix B GFSbox — AES-128 with all-zero key *) -(* Source: "The Advanced Encryption Standard Algorithm Validation Suite" *) +(* KAT: AESAVS Appendix B GFSbox — AES-128 with all-zero key *) +(* Source: "The Advanced Encryption Standard Algorithm Validation Suite" *) (* ========================================================================= *) let AESAVS_ZERO_KEY_128_SCHEDULE = new_definition @@ -477,7 +477,7 @@ prove(`aes128_cipher (word 0x00000000000000000000000000000000) AESAVS_ZERO_KEY_128_SCHEDULE)) THEN REFL_TAC);; (* ========================================================================= *) -(* KAT: AES-256 with all-zero key *) +(* KAT: AES-256 with all-zero key *) (* ========================================================================= *) let AESAVS_ZERO_KEY_256_SCHEDULE = new_definition From a2333098bf47e2cb663aa454d41d9e5d96290e78 Mon Sep 17 00:00:00 2001 From: sanketh Date: Wed, 8 Apr 2026 16:22:28 +0000 Subject: [PATCH 3/7] Add S-box/FFmul precomputation tables and fast AES conversions Precompute all 768 lookup table entries (256 each for S-box, FFmul02, FFmul03) as proven theorems at load time (~48s). This eliminates the word_subword bottleneck on 2048-bit constants, reducing AES-128 evaluation from ~40s to ~7s per call. Add FIPS197_ENCRYPT_FAST_CONV and supporting fast conversion chain. Uncomment all KATs (key expansion, SubBytes, ShiftRows, MixColumns, AddRoundKey, full AES-128 and AES-256 cipher) using fast conversions. Remove fips197_add_round_key (just word_xor, unused). --- common/fips197.ml | 109 ++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 91 insertions(+), 18 deletions(-) diff --git a/common/fips197.ml b/common/fips197.ml index c0cc867ac..93110d807 100644 --- a/common/fips197.ml +++ b/common/fips197.ml @@ -276,19 +276,11 @@ prove(`fips197_mix_columns (word 0xd4bf5d30e0b452aeb84111f11e2798e5) = word 0x046681e5e0cb199a48f8d37a2806264c`, CONV_TAC(LAND_CONV FIPS197_MIX_COLUMNS_CONV) THEN REFL_TAC);; -(* ========================================================================= *) -(* AddRoundKey (FIPS 197 Sec 5.1.4): XOR state with round key. *) -(* ========================================================================= *) - -let fips197_add_round_key = new_definition - `fips197_add_round_key (s:128 word) (k:128 word) : 128 word = word_xor s k`;; - -(* KAT: FIPS 197 Appendix B, Round 1 AddRoundKey *) -prove(`fips197_add_round_key (word 0x046681e5e0cb199a48f8d37a2806264c) - (word 0xa0fafe1788542cb123a339392a6c7605) = +(* KAT: FIPS 197 Appendix B, Round 1 AddRoundKey (just XOR) *) +prove(`word_xor (word 0x046681e5e0cb199a48f8d37a2806264c : 128 word) + (word 0xa0fafe1788542cb123a339392a6c7605 : 128 word) = word 0xa49c7ff2689f352b6b5bea43026a5049`, - CONV_TAC(REWRITE_CONV [fips197_add_round_key] THENC - DEPTH_CONV WORD_RED_CONV) THEN REFL_TAC);; + CONV_TAC(DEPTH_CONV WORD_RED_CONV) THEN REFL_TAC);; (* ========================================================================= *) (* AES Cipher (FIPS 197 Algorithm 1) — unrolled *) @@ -381,6 +373,87 @@ let FIPS197_ENCRYPT_CONV cipher_def ks_def = DEPTH_CONV FIPS197_ROUND_REDUCE_CONV THENC FIPS197_FINAL_ROUND_REDUCE_CONV;; +(* ========================================================================= *) +(* Fast AES conversions via precomputed lookup tables. *) +(* *) +(* The bottleneck in AES evaluation is word_subword on 2048-bit constants *) +(* (joined_GF2 for S-box, joined_FFmul_02/03 for MixColumns). *) +(* Precomputing all 256 entries for each table eliminates this bottleneck. *) +(* One-time cost: ~48s. Speedup: AES-128 from ~40s to ~7s per call. *) +(* ========================================================================= *) + +let aes_sbox_table = Array.init 256 (fun n -> + AES_SUB_BYTE_CONV + (vsubst [mk_small_numeral n, `n:num`] + `aes_sub_byte joined_GF2 ((word:num->8 word) n)`));; + +let ffmul02_table = Array.init 256 (fun n -> + FFMUL02_CONV + (vsubst [mk_small_numeral n, `n:num`] + `FFmul02 ((word:num->8 word) n)`));; + +let ffmul03_table = Array.init 256 (fun n -> + FFMUL03_CONV + (vsubst [mk_small_numeral n, `n:num`] + `FFmul03 ((word:num->8 word) n)`));; + +let FIPS197_SUB_BYTES_FAST_CONV = + REWRITE_CONV [fips197_sub_bytes; aes_sub_bytes; aes_sub_bytes_select] THENC + TOP_DEPTH_CONV let_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV) THENC + GEN_REWRITE_CONV ONCE_DEPTH_CONV (Array.to_list aes_sbox_table) THENC + WORD_JOIN_LIST_16_8_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +let AES_MIX_WORD_FAST_CONV = + REWRITE_CONV [aes_mix_word] THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV) THENC + GEN_REWRITE_CONV ONCE_DEPTH_CONV (Array.to_list ffmul02_table) THENC + GEN_REWRITE_CONV ONCE_DEPTH_CONV (Array.to_list ffmul03_table) THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +let FIPS197_MIX_COLUMNS_FAST_CONV = + REWRITE_CONV [fips197_mix_columns] THENC + AES_MIX_WORD_FAST_CONV THENC + WORD_JOIN_LIST_16_8_CONV THENC + TOP_DEPTH_CONV let_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +let FIPS197_ROUND_FAST_CONV = + REWRITE_CONV [fips197_round] THENC + FIPS197_SUB_BYTES_FAST_CONV THENC + FIPS197_SHIFT_ROWS_CONV THENC + FIPS197_MIX_COLUMNS_FAST_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +let FIPS197_ROUND_REDUCE_FAST_CONV tm = + match tm with + Comb(Comb(Const("fips197_round",_),Comb(Const("word",_),s)), + Comb(Const("word",_),k)) + when is_numeral s && is_numeral k -> FIPS197_ROUND_FAST_CONV tm + | _ -> failwith "FIPS197_ROUND_REDUCE_FAST_CONV";; + +let FIPS197_FINAL_ROUND_FAST_CONV = + REWRITE_CONV [fips197_final_round] THENC + FIPS197_SUB_BYTES_FAST_CONV THENC + FIPS197_SHIFT_ROWS_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +let FIPS197_FINAL_ROUND_REDUCE_FAST_CONV tm = + match tm with + Comb(Comb(Const("fips197_final_round",_),Comb(Const("word",_),s)), + Comb(Const("word",_),k)) + when is_numeral s && is_numeral k -> FIPS197_FINAL_ROUND_FAST_CONV tm + | _ -> failwith "FIPS197_FINAL_ROUND_REDUCE_FAST_CONV";; + +let FIPS197_ENCRYPT_FAST_CONV cipher_def ks_def = + REWRITE_CONV [ks_def] THENC + REWRITE_CONV [cipher_def] THENC + TOP_DEPTH_CONV let_CONV THENC + DEPTH_CONV (EL_CONV ORELSEC WORD_RED_CONV ORELSEC NUM_RED_CONV) THENC + DEPTH_CONV FIPS197_ROUND_REDUCE_FAST_CONV THENC + FIPS197_FINAL_ROUND_REDUCE_FAST_CONV;; + (* ========================================================================= *) (* KAT: FIPS 197 Appendix B — AES-128 full encryption *) (* Plaintext: 0x3243f6a8885a308d313198a2e0370734 *) @@ -406,7 +479,7 @@ let AES128_APPENDIX_B_KEY_SCHEDULE = new_definition prove(`aes128_cipher (word 0x3243f6a8885a308d313198a2e0370734) AES128_APPENDIX_B_KEY_SCHEDULE = word 0x3925841d02dc09fbdc118597196a0b32`, - CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes128_cipher + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_FAST_CONV aes128_cipher AES128_APPENDIX_B_KEY_SCHEDULE)) THEN REFL_TAC);; (* ========================================================================= *) @@ -439,7 +512,7 @@ let AES256_CORE_KEY_SCHEDULE = new_definition prove(`aes256_cipher (word 0x6bc1bee22e409f96e93d7e117393172a) AES256_CORE_KEY_SCHEDULE = word 0xf3eed1bdb5d2a03c064b5a7e3db181f8`, - CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes256_cipher + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_FAST_CONV aes256_cipher AES256_CORE_KEY_SCHEDULE)) THEN REFL_TAC);; (* ========================================================================= *) @@ -466,14 +539,14 @@ let AESAVS_ZERO_KEY_128_SCHEDULE = new_definition prove(`aes128_cipher (word 0xf34481ec3cc627bacd5dc3fb08f273e6) AESAVS_ZERO_KEY_128_SCHEDULE = word 0x0336763e966d92595a567cc9ce537f5e`, - CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes128_cipher + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_FAST_CONV aes128_cipher AESAVS_ZERO_KEY_128_SCHEDULE)) THEN REFL_TAC);; (* AESAVS: key=0, pt=0 *) prove(`aes128_cipher (word 0x00000000000000000000000000000000) AESAVS_ZERO_KEY_128_SCHEDULE = word 0x66e94bd4ef8a2c3b884cfa59ca342b2e`, - CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes128_cipher + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_FAST_CONV aes128_cipher AESAVS_ZERO_KEY_128_SCHEDULE)) THEN REFL_TAC);; (* ========================================================================= *) @@ -503,12 +576,12 @@ let AESAVS_ZERO_KEY_256_SCHEDULE = new_definition prove(`aes256_cipher (word 0x00000000000000000000000000000000) AESAVS_ZERO_KEY_256_SCHEDULE = word 0xdc95c078a2408989ad48a21492842087`, - CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes256_cipher + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_FAST_CONV aes256_cipher AESAVS_ZERO_KEY_256_SCHEDULE)) THEN REFL_TAC);; (* AESAVS GFSbox first vector: key=0, pt=014730f8... *) prove(`aes256_cipher (word 0x014730f80ac625fe84f026c60bfd547d) AESAVS_ZERO_KEY_256_SCHEDULE = word 0x5c9d844ed46f9885085e5d6a4f94c7d7`, - CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_CONV aes256_cipher + CONV_TAC(LAND_CONV(FIPS197_ENCRYPT_FAST_CONV aes256_cipher AESAVS_ZERO_KEY_256_SCHEDULE)) THEN REFL_TAC);; From 6154292ca84a80f67e8b2a1644b047a79292ddbe Mon Sep 17 00:00:00 2001 From: sanketh Date: Wed, 8 Apr 2026 19:32:23 +0000 Subject: [PATCH 4/7] Pick common/misc.ml from #381 (word_pmul) Cherry-pick common/misc.ml from s2n-bignum#381 to get word_pmul and WORD_PMUL_CONV, needed by ghash_reduce in common/ghash.ml. This file should be identical to the version in #381 and will be a no-op when #381 merges. --- common/misc.ml | 169 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 169 insertions(+) diff --git a/common/misc.ml b/common/misc.ml index 6a0726cfb..4e394dd82 100644 --- a/common/misc.ml +++ b/common/misc.ml @@ -1664,6 +1664,175 @@ let WORD_CONDENSE_CONV = extra_word_CONV := WORD_CONDENSE_CONV::(!extra_word_CONV);; +(* ------------------------------------------------------------------------- *) +(* Multiplication of binary polynomials as words, "carryless multiplication" *) +(* ------------------------------------------------------------------------- *) + +let word_pmul = define + `(word_pmul:M word->N word->P word) x y = + word_of_bits {k | ODD(CARD {i | i <= k /\ bit i x /\ bit (k - i) y})}`;; + +let BIT_WORD_PMUL_ALT = prove + (`!x y k. bit k ((word_pmul:M word->N word->P word) x y) <=> + k < dimindex(:P) /\ + ODD(CARD {i | i <= k /\ bit i x /\ bit (k - i) y})`, + REWRITE_TAC[word_pmul; BIT_WORD_OF_BITS; IN_ELIM_THM]);; + +let BIT_WORD_PMUL = prove + (`!x y k. bit k ((word_pmul:M word->N word->P word) x y) <=> + k < dimindex(:P) /\ + ODD(nsum (0..k) (\i. bitval(bit i x) * bitval(bit (k - i) y)))`, + REPEAT GEN_TAC THEN REWRITE_TAC[BIT_WORD_PMUL_ALT] THEN + AP_TERM_TAC THEN REWRITE_TAC[GSYM BITVAL_AND] THEN + REWRITE_TAC[bitval; GSYM NSUM_RESTRICT_SET] THEN + SIMP_TAC[NSUM_CONST; FINITE_RESTRICT; FINITE_NUMSEG] THEN + REWRITE_TAC[MULT_CLAUSES; LE_0; IN_NUMSEG]);; + +let BITVAL_BIT_WORD_PMUL = prove + (`!x y k. bitval(bit k ((word_pmul:M word->N word->P word) x y)) = + if k < dimindex(:P) + then nsum(0..k) (\i. bitval(bit i x) * bitval(bit (k - i) y)) MOD 2 + else 0`, + REPEAT GEN_TAC THEN REWRITE_TAC[BIT_WORD_PMUL] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES; BITVAL_ODD]);; + +let WORD_PMUL_0 = prove + (`(!y. (word_pmul:M word->N word->P word) (word 0) y = word 0) /\ + (!x. (word_pmul:M word->N word->P word) x (word 0) = word 0)`, + REWRITE_TAC[word_pmul; BIT_WORD_0; MULT_CLAUSES; EMPTY_GSPEC; + CARD_CLAUSES; ODD; WORD_OF_BITS_EMPTY]);; + +let WORD_PMUL_XOR = prove + (`(!x y z. (word_pmul:M word->N word->P word) (word_xor x y) z = + word_xor (word_pmul x z) (word_pmul y z)) /\ + (!x y z. (word_pmul:M word->N word->P word) x (word_xor y z) = + word_xor (word_pmul x y) (word_pmul x z))`, + REPEAT STRIP_TAC THEN + GEN_REWRITE_TAC I [WORD_EQ_BITS_ALT] THEN + REWRITE_TAC[BIT_WORD_PMUL; BIT_WORD_XOR_ALT] THEN + X_GEN_TAC `i:num` THEN DISCH_TAC THEN + ASM_REWRITE_TAC[GSYM ODD_ADD] THEN + REWRITE_TAC[MESON[ODD_ADD; NOT_ODD] `(ODD x <=> ODD y) <=> EVEN(x + y)`] THEN + REWRITE_TAC[GSYM NSUM_ADD_NUMSEG] THEN + MATCH_MP_TAC(ISPEC `EVEN` NSUM_CLOSED) THEN + SIMP_TAC[EVEN; EVEN_ADD] THEN X_GEN_TAC `j:num` THEN DISCH_TAC THEN + REWRITE_TAC[IN_NUMSEG; LE_0; BITVAL_XOR] THEN + REWRITE_TAC[bitval] THEN + REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN + CONV_TAC NUM_REDUCE_CONV);; + +let WORD_PMUL_ZX = prove + (`(!x y. word_pmul (word_zx x:P word) y = + (word_pmul:M word->N word->P word) x y) /\ + (!x y. word_pmul x (word_zx y:P word) = + (word_pmul:M word->N word->P word) x y)`, + REPEAT STRIP_TAC THEN REWRITE_TAC[word_pmul; BIT_WORD_ZX] THEN + GEN_REWRITE_TAC I [WORD_OF_BITS_EQ] THEN SIMP_TAC[IN_ELIM_THM] THEN + REPEAT STRIP_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN + GEN_REWRITE_TAC I [EXTENSION] THEN GEN_TAC THEN + REWRITE_TAC[IN_ELIM_THM] THEN + EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC);; + +let WORD_PMUL_STEP = prove + (`!x y. (word_pmul:M word->N word->N word) x y = + word_xor (if bit 0 x then y else word 0) + (word_pmul (word_ushr x 1) (word_shl y 1))`, + REPEAT GEN_TAC THEN GEN_REWRITE_TAC I [WORD_EQ_BITS_ALT] THEN + X_GEN_TAC `i:num` THEN DISCH_TAC THEN + ASM_REWRITE_TAC[BIT_WORD_XOR; BIT_WORD_PMUL] THEN + REWRITE_TAC[TAUT `(p <=> ~(q <=> r)) <=> ~(p <=> r) <=> q`] THEN + REWRITE_TAC[GSYM ODD_ADD] THEN + REWRITE_TAC[BIT_WORD_USHR; BIT_WORD_SHL] THEN + ASM_SIMP_TAC[ARITH_RULE `i:num < N ==> i - j < N`] THEN + REWRITE_TAC[ARITH_RULE `i - j - 1 = i - (j + 1)`] THEN + REWRITE_TAC[ARITH_RULE `1 <= i - j <=> j + 1 <= i`] THEN + REWRITE_TAC[GSYM(SPEC `1` NSUM_OFFSET)] THEN + SIMP_TAC[NSUM_CLAUSES_LEFT; LE_0] THEN REWRITE_TAC[ADD_CLAUSES] THEN + REWRITE_TAC[GSYM ADD1; NSUM_CLAUSES_NUMSEG; ARITH_RULE `1 <= SUC n`] THEN + SIMP_TAC[ARITH_RULE `~(SUC i <= i)`; BITVAL_CLAUSES; MULT_CLAUSES] THEN + REWRITE_TAC[ADD_CLAUSES; ARITH_RULE `(i + j) + j = 2 * j + i`] THEN + REWRITE_TAC[ODD_ADD; ODD_MULT; ARITH_ODD; SUB_0] THEN + REWRITE_TAC[bitval] THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN + REWRITE_TAC[BIT_WORD_0] THEN CONV_TAC NUM_REDUCE_CONV);; + +let WORD_PMUL_SYM = prove + (`!x y. (word_pmul:M word->M word->N word) x y = word_pmul y x`, + REPEAT GEN_TAC THEN REWRITE_TAC[WORD_EQ_BITS_ALT] THEN + REWRITE_TAC[BIT_WORD_PMUL] THEN X_GEN_TAC `i:num` THEN DISCH_TAC THEN + GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [NSUM_REFLECT] THEN + ASM_SIMP_TAC[LT; SUB_0; ARITH_RULE `j:num <= i ==> i - (i - j) = j`] THEN + REWRITE_TAC[MULT_SYM]);; + +let WORD_PMUL_POW2 = prove + (`(!(x:N word) n. word_pmul (word(2 EXP n):N word) x = word_shl x n) /\ + (!(x:N word) n. word_pmul x (word(2 EXP n):N word) = word_shl x n)`, + GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [WORD_PMUL_SYM] THEN + REWRITE_TAC[] THEN REPEAT GEN_TAC THEN + ONCE_REWRITE_TAC[WORD_EQ_BITS_ALT] THEN + X_GEN_TAC `i:num` THEN DISCH_TAC THEN + ASM_REWRITE_TAC[BIT_WORD_PMUL; BIT_WORD_SHL; BIT_WORD_POW2] THEN + REWRITE_TAC[GSYM BITVAL_AND] THEN + REWRITE_TAC[GSYM CONJ_ASSOC; bitval] THEN + ONCE_REWRITE_TAC[MESON[] + `(if p /\ q then 1 else 0) = if p then (if q then 1 else 0) else 0`] THEN + SIMP_TAC[NSUM_DELTA; IN_NUMSEG; LE_0] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[ODD] THEN + ONCE_REWRITE_TAC[COND_RAND] THEN + REWRITE_TAC[ARITH_ODD; TAUT `(if x then T else F) <=> x`] THEN + MATCH_MP_TAC(TAUT `p ==> (p /\ q <=> q)`) THEN ASM_ARITH_TAC);; + +let WORD_PMUL_CONV = + let in_conv = + GEN_REWRITE_CONV I [GSYM(CONJUNCT2 WORD_PMUL_ZX)] THENC + RAND_CONV WORD_ZX_CONV + and base_conv = + GEN_REWRITE_CONV I [CONJUNCT2 WORD_PMUL_0] + and step_conv = + GEN_REWRITE_CONV I [WORD_PMUL_STEP] THENC + BINOP2_CONV + (RATOR_CONV(LAND_CONV BIT_WORD_CONV) THENC + GEN_REWRITE_CONV I [COND_CLAUSES]) + (BINOP2_CONV (WORD_USHR_CONV) WORD_SHL_CONV) in + let rec conv tm = + try base_conv tm with Failure _ -> + (step_conv THENC RAND_CONV conv THENC WORD_XOR_CONV) tm in + let fullconv = in_conv THENC conv in + fun tm -> + match tm with + Comb(Comb(Const("word_pmul",_), + Comb(Const("word",_),m)), + Comb(Const("word",_),n)) + when is_numeral m && is_numeral n -> fullconv tm + | _ -> failwith "WORD_PMUL_CONV";; + +let BIT_WORD_PMUL_CONV = + let main_conv = + RAND_CONV + (EXPAND_NSUM_CONV THENC + DEPTH_BINOP_CONV `(+):num->num->num` + (BINOP2_CONV + (RAND_CONV WORD_BIT_CONV THENC GEN_REWRITE_CONV I [BITVAL_CLAUSES]) + (RAND_CONV(LAND_CONV NUM_SUB_CONV THENC WORD_BIT_CONV) THENC + GEN_REWRITE_CONV I [BITVAL_CLAUSES]) THENC + NUM_MULT_CONV) THENC + DEPTH_CONV NUM_ADD_CONV) THENC + NUM_ODD_CONV in + let conv = + GEN_REWRITE_CONV I [BIT_WORD_PMUL] THENC + LAND_CONV(RAND_CONV DIMINDEX_CONV THENC NUM_LT_CONV) THENC + ((GEN_REWRITE_CONV I [TAUT `T /\ p <=> p`] THENC main_conv) ORELSEC + GEN_REWRITE_CONV I [TAUT `F /\ p <=> F`]) in + fun tm -> + match tm with + Comb(Comb(Const("bit",_),i), + Comb(Comb(Const("word_pmul",_), + Comb(Const("word",_),m)), + Comb(Const("word",_),n))) + when is_numeral i && is_numeral m && is_numeral n -> conv tm + | _ -> failwith "BIT_WORD_PMUL_CONV";; + +extra_word_CONV := WORD_PMUL_CONV::(!extra_word_CONV);; + (* ------------------------------------------------------------------------- *) (* A few more lemmas about words. *) (* ------------------------------------------------------------------------- *) From 1ba8858bb22e713400d40ef9971367b39427f56f Mon Sep 17 00:00:00 2001 From: sanketh Date: Wed, 8 Apr 2026 19:32:31 +0000 Subject: [PATCH 5/7] Pick common/ghash.ml from #382 (GHASH polynomial reduction) Cherry-pick common/ghash.ml from s2n-bignum#382 to get ghash_reduce1, ghash_reduce, and their correctness proofs. Needed by gf128_mul in common/gcm.ml. This file should be identical to the version in #382 and will be a no-op when #382 merges. --- common/ghash.ml | 645 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 645 insertions(+) create mode 100644 common/ghash.ml diff --git a/common/ghash.ml b/common/ghash.ml new file mode 100644 index 000000000..361aa5b18 --- /dev/null +++ b/common/ghash.ml @@ -0,0 +1,645 @@ +(* ========================================================================= *) +(* GHASH polynomial both via machine words and as an element of GF(2)[X]. *) +(* ========================================================================= *) + +needs "common/misc.ml";; +needs "Library/rabin_test.ml";; + +(* ------------------------------------------------------------------------- *) +(* General trivia *) +(* ------------------------------------------------------------------------- *) + +let BOOL_RING_SUB = prove + (`ring_sub bool_ring = \x y. ~(x <=> y)`, + SIMP_TAC[FUN_EQ_THM; ring_sub; BOOL_RING; I_DEF]);; + +let POLY_RING_VAR_POW_1 = prove + (`!(r:A ring) i. + ring_pow (poly_ring r (:1)) (poly_var r i) k = + \m. if m = \j. k then ring_1 r else ring_0 r`, + REWRITE_TAC[POLY_RING_VAR_POW] THEN + REWRITE_TAC[MESON[one] `i:1 = j <=> T`]);; + +(* ------------------------------------------------------------------------- *) +(* Some basics for univariate polynomials to be less tiresome. *) +(* The library theory of polynomials has some cruft for arbitrary monomials. *) +(* ------------------------------------------------------------------------- *) + +let coeff = define + `coeff:num->1->num = \d v. d`;; + +let POLY_MUL_UNIVARIATE = prove + (`!r (p:(1->num)->R) q. + poly_mul r p q = + \m. ring_sum r (0..m one) + (\i. ring_mul r (p(coeff i)) (q(coeff(m one - i))))`, + REPEAT GEN_TAC THEN REWRITE_TAC[poly_mul; coeff] THEN + GEN_REWRITE_TAC I [FUN_EQ_THM] THEN + GEN_REWRITE_TAC I [FORALL_FUN_FROM_1] THEN + X_GEN_TAC `k:num` THEN REWRITE_TAC[] THEN + MATCH_MP_TAC RING_SUM_EQ_GENERAL_INVERSES THEN + EXISTS_TAC `\mm. (FST:(1->num)#(1->num)->1->num) mm one` THEN + EXISTS_TAC `\i. (\v:1. i),(\v:1. k - i)` THEN + REWRITE_TAC[FORALL_IN_GSPEC; IN_ELIM_PAIR_THM] THEN + REWRITE_TAC[FORALL_FUN_FROM_1; coeff; monomial_mul] THEN + REWRITE_TAC[MESON[] `(\x:1. a) = (\x. b) <=> a = b`] THEN + REWRITE_TAC[IN_NUMSEG; LE_0] THEN + SIMP_TAC[ARITH_RULE `i + j:num = k <=> i <= k /\ j = k - i`]);; + +(* ------------------------------------------------------------------------- *) +(* A lemma for mapping between integer and boolean points of view *) +(* ------------------------------------------------------------------------- *) + +let BITVAL_RING_SUM_BOOL_RING = prove + (`!f (s:K->bool). + FINITE s + ==> bitval(ring_sum bool_ring s f) = nsum s (bitval o f) MOD 2`, + GEN_TAC THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN + MATCH_MP_TAC FINITE_INDUCT_STRONG THEN + SIMP_TAC[NSUM_CLAUSES; RING_SUM_CLAUSES; BOOL_RING; IN_UNIV] THEN + REWRITE_TAC[BITVAL_CLAUSES] THEN CONV_TAC NUM_REDUCE_CONV THEN + ONCE_REWRITE_TAC[GSYM MOD_ADD_MOD] THEN + MAP_EVERY X_GEN_TAC [`a:K`; `s:K->bool`] THEN STRIP_TAC THEN + ASM_REWRITE_TAC[BITVAL_NOT; BITVAL_IFF; BITVAL_CLAUSES] THEN + REWRITE_TAC[o_THM; bitval] THEN + REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN + CONV_TAC NUM_REDUCE_CONV);; + +(* ------------------------------------------------------------------------- *) +(* Correspondence between binary polynomials and machine words. *) +(* Polynomials are members of `poly_ring bool_ring (:1)` = GF(2)[X]. *) +(* They are mapped to and from machine words of length N, type `:N word`. *) +(* ------------------------------------------------------------------------- *) + +let bool_poly = define + `bool_poly = poly_ring bool_ring (:1)`;; + +let BOOL_POLY_NEG = prove + (`ring_neg bool_poly = I`, + REWRITE_TAC[FUN_EQ_THM; bool_poly; POLY_RING; BOOL_RING; poly_neg; I_DEF]);; + +let BOOL_POLY_SUB = prove + (`ring_sub bool_poly = ring_add bool_poly`, + REWRITE_TAC[FUN_EQ_THM; bool_poly; POLY_RING_CLAUSES; + BOOL_RING; poly_add; poly_sub; BOOL_RING_SUB]);; + +let POLY_VAR_BOOL_POLY = prove + (`poly_var bool_ring one IN ring_carrier bool_poly`, + REWRITE_TAC[bool_poly; POLY_VAR; IN_UNIV]);; + +let POLY_VARPOW_BOOL_POLY = prove + (`!n. ring_pow bool_poly (poly_var bool_ring one) n IN ring_carrier bool_poly`, + SIMP_TAC[RING_POW; POLY_VAR_BOOL_POLY]);; + +let word_of_poly = define + `(word_of_poly:((1->num)->bool)->N word) p = word_of_bits {i | p(coeff i)}`;; + +let poly_of_word = define + `(poly_of_word:N word->(1->num)->bool) w = \m. bit (m one) w`;; + +let BOOL_POLY_OF_WORD = prove + (`!w:N word. poly_of_word w IN ring_carrier bool_poly`, + REWRITE_TAC[bool_poly; POLY_RING; ring_polynomial; ring_powerseries; + IN_ELIM_THM; BOOL_RING; SUBSET_UNIV; IN_UNIV] THEN + REWRITE_TAC[FINITE_MONOMIAL_VARS_1; INFINITE] THEN + REWRITE_TAC[poly_of_word] THEN GEN_TAC THEN + MATCH_MP_TAC FINITE_SUBSET THEN + EXISTS_TAC `IMAGE coeff {i | i < dimindex(:N)}` THEN + SIMP_TAC[FINITE_IMAGE; FINITE_NUMSEG_LT; SUBSET; IN_ELIM_THM] THEN + REWRITE_TAC[FORALL_FUN_FROM_1; IN_IMAGE; IN_ELIM_THM; coeff] THEN + MESON_TAC[BIT_TRIVIAL; NOT_LE]);; + +let RING_POLYNOMIAL_OF_WORD = prove + (`!w:N word. ring_polynomial bool_ring (poly_of_word w)`, + REWRITE_TAC[RING_POLYNOMIAL; GSYM bool_poly; BOOL_POLY_OF_WORD]);; + +let POLY_DEG_POLY_OF_WORD = prove + (`!w:N word. + poly_deg bool_ring (poly_of_word w) = + dimindex(:N) - 1 - word_clz w`, + GEN_TAC THEN MATCH_MP_TAC POLY_DEG_UNIQUE THEN + REWRITE_TAC[RING_POLYNOMIAL_OF_WORD] THEN + REWRITE_TAC[MONOMIAL_DEG_UNIVARIATE; poly_of_word] THEN + SIMP_TAC[FORALL_FUN_FROM_1; EXISTS_FUN_FROM_1; MONOMIAL_DEG_UNIVARIATE] THEN + REWRITE_TAC[BOOL_RING] THEN + SIMP_TAC[WORD_CLZ_LBOUND_ALT; ARITH_RULE `c + i < n ==> i <= n - 1 - c`] THEN + ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[UNWIND_THM2] THEN + MP_TAC(ISPECL [`w:N word`; `word_clz(w:N word)`] WORD_CLZ_UNIQUE) THEN + REWRITE_TAC[ARITH_RULE `n - 1 - w = n - w - 1`] THEN + ASM_CASES_TAC `bit (dimindex(:N) - word_clz w - 1) (w:N word)` THEN + ASM_REWRITE_TAC[] THEN ARITH_TAC);; + +let POLY_DEG_POLY_OF_WORD_BOUND = prove + (`!w:N word. poly_deg bool_ring (poly_of_word w) < dimindex(:N)`, + GEN_TAC THEN + SIMP_TAC[DIMINDEX_NONZERO; ARITH_RULE + `~(n = 0) ==> (x < n <=> x <= n - 1)`] THEN + MATCH_MP_TAC POLY_DEG_LE THEN + REWRITE_TAC[RING_POLYNOMIAL; BOOL_POLY_OF_WORD; GSYM bool_poly] THEN + REWRITE_TAC[FORALL_FUN_FROM_1; BOOL_RING; MONOMIAL_DEG_UNIVARIATE] THEN + REWRITE_TAC[poly_of_word; coeff] THEN + ONCE_REWRITE_TAC[BIT_GUARD] THEN ARITH_TAC);; + +let WORD_OF_POLY_OF_WORD = prove + (`!w:N word. word_of_poly (poly_of_word w) = w`, + GEN_TAC THEN REWRITE_TAC[word_of_poly; poly_of_word] THEN + GEN_REWRITE_TAC I [WORD_EQ_BITS_ALT] THEN + SIMP_TAC[BIT_WORD_OF_BITS; coeff; IN_ELIM_THM]);; + +let WORD_OF_POLY_OF_WORD_GEN = prove + (`!w:N word. word_of_poly (poly_of_word w):M word = word_zx w`, + GEN_TAC THEN REWRITE_TAC[word_of_poly; poly_of_word] THEN + GEN_REWRITE_TAC I [WORD_EQ_BITS_ALT] THEN + SIMP_TAC[BIT_WORD_OF_BITS; BIT_WORD_ZX; coeff; IN_ELIM_THM]);; + +let POLY_OF_WORD_OF_POLY = prove + (`!p. p IN ring_carrier bool_poly /\ + poly_deg bool_ring p < dimindex(:N) + ==> poly_of_word (word_of_poly p:N word) = p`, + REWRITE_TAC[bool_poly; GSYM RING_POLYNOMIAL] THEN + REPEAT STRIP_TAC THEN + FIRST_X_ASSUM(MP_TAC o SPEC `dimindex(:N)` o MATCH_MP POLY_DEG_GE_EQ) THEN + ASM_REWRITE_TAC[GSYM NOT_LT; DE_MORGAN_THM; NOT_EXISTS_THM] THEN + DISCH_THEN(MP_TAC o CONJUNCT2) THEN + GEN_REWRITE_TAC RAND_CONV [FUN_EQ_THM] THEN + REWRITE_TAC[FORALL_FUN_FROM_1; word_of_poly; poly_of_word] THEN + REWRITE_TAC[BIT_WORD_OF_BITS; coeff; BOOL_RING; MONOMIAL_DEG_UNIVARIATE] THEN + SET_TAC[]);; + +let POLY_OF_WORD_ZX = prove + (`!x. dimindex(:M) <= dimindex(:N) + ==> poly_of_word((word_zx:M word->N word) x) = poly_of_word x`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[GSYM WORD_OF_POLY_OF_WORD_GEN] THEN + MATCH_MP_TAC POLY_OF_WORD_OF_POLY THEN + ASM_MESON_TAC[POLY_DEG_POLY_OF_WORD_BOUND; LTE_TRANS; BOOL_POLY_OF_WORD]);; + +let POLY_OF_WORD_OF_POLY_EQ = prove + (`!p. p IN ring_carrier bool_poly + ==> (poly_of_word (word_of_poly p:N word) = p <=> + poly_deg bool_ring p < dimindex(:N))`, + MESON_TAC[POLY_OF_WORD_OF_POLY; POLY_DEG_POLY_OF_WORD_BOUND]);; + +(* ------------------------------------------------------------------------- *) +(* XOR and PMUL correspond to addition and multiplication of polynomials. *) +(* ------------------------------------------------------------------------- *) + +let POLY_OF_WORD_0 = prove + (`poly_of_word (word 0:N word) = ring_0 bool_poly`, + REWRITE_TAC[poly_of_word; bool_poly; BIT_WORD_0; POLY_0] THEN + REWRITE_TAC[POLY_RING; BOOL_RING; POLY_0]);; + +let POLY_OF_WORD_1 = prove + (`poly_of_word (word 1:N word) = ring_1 bool_poly`, + REWRITE_TAC[poly_of_word; bool_poly; BIT_WORD_1; POLY_RING; poly_1] THEN + REWRITE_TAC[BOOL_RING; poly_const; monomial_1] THEN + REWRITE_TAC[MESON[] `(if p then T else F) <=> p`] THEN + GEN_REWRITE_TAC I [FUN_EQ_THM] THEN REWRITE_TAC[FORALL_FUN_FROM_1] THEN + REWRITE_TAC[FUN_EQ_THM]);; + +let WORD_XOR_POLY = prove + (`!x y:N word. + word_xor x y = + word_of_poly (ring_add bool_poly (poly_of_word x) (poly_of_word y))`, + REPEAT GEN_TAC THEN + GEN_REWRITE_TAC I [WORD_EQ_BITS_ALT] THEN + X_GEN_TAC `i:num` THEN DISCH_TAC THEN + REWRITE_TAC[word_of_poly; bool_poly; POLY_RING; BOOL_RING; poly_add] THEN + REWRITE_TAC[BIT_WORD_OF_BITS; IN_ELIM_THM; BIT_WORD_XOR] THEN + REWRITE_TAC[poly_of_word; coeff]);; + +let POLY_OF_WORD_XOR = prove + (`!(x:N word) (y:N word). + poly_of_word(word_xor x y) = + ring_add bool_poly (poly_of_word x) (poly_of_word y)`, + REPEAT GEN_TAC THEN REWRITE_TAC[WORD_XOR_POLY] THEN + MATCH_MP_TAC POLY_OF_WORD_OF_POLY THEN + SIMP_TAC[RING_ADD; BOOL_POLY_OF_WORD] THEN + REWRITE_TAC[bool_poly; POLY_RING] THEN + W(MP_TAC o PART_MATCH (lhand o rand) POLY_DEG_ADD_LE o lhand o snd) THEN + REWRITE_TAC[RING_POLYNOMIAL; BOOL_POLY_OF_WORD; GSYM bool_poly] THEN + MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] LET_TRANS) THEN + MATCH_MP_TAC(ARITH_RULE `x < n /\ y < n ==> MAX x y < n`) THEN + REWRITE_TAC[POLY_DEG_POLY_OF_WORD_BOUND]);; + +let WORD_PMUL_POLY = prove + (`!x y. (word_pmul:M word->N word->P word) x y = + word_of_poly (ring_mul bool_poly (poly_of_word x) (poly_of_word y))`, + REPEAT GEN_TAC THEN + GEN_REWRITE_TAC I [WORD_EQ_BITS_ALT] THEN + X_GEN_TAC `i:num` THEN DISCH_TAC THEN + ASM_REWRITE_TAC[GSYM EQ_BITVAL; BITVAL_BIT_WORD_PMUL] THEN + REWRITE_TAC[word_of_poly; bool_poly; POLY_RING] THEN + ASM_REWRITE_TAC[POLY_MUL_UNIVARIATE; BIT_WORD_OF_BITS; IN_ELIM_THM] THEN + REWRITE_TAC[coeff; BOOL_RING] THEN + SIMP_TAC[BITVAL_RING_SUM_BOOL_RING; FINITE_NUMSEG] THEN + REWRITE_TAC[o_DEF; BITVAL_AND; poly_of_word]);; + +let POLY_OF_WORD_PMUL_2N = prove + (`!(x:N word) (y:N word). + poly_of_word(word_pmul x y:((N)tybit0)word) = + ring_mul bool_poly (poly_of_word x) (poly_of_word y)`, + REPEAT GEN_TAC THEN REWRITE_TAC[WORD_PMUL_POLY] THEN + MATCH_MP_TAC POLY_OF_WORD_OF_POLY THEN + SIMP_TAC[RING_MUL; BOOL_POLY_OF_WORD; DIMINDEX_TYBIT0] THEN + REWRITE_TAC[bool_poly; POLY_RING] THEN + W(MP_TAC o PART_MATCH (lhand o rand) POLY_DEG_MUL_LE o lhand o snd) THEN + REWRITE_TAC[RING_POLYNOMIAL; BOOL_POLY_OF_WORD; GSYM bool_poly] THEN + MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] LET_TRANS) THEN + MATCH_MP_TAC(ARITH_RULE `x < n /\ y < n ==> x + y < 2 * n`) THEN + REWRITE_TAC[POLY_DEG_POLY_OF_WORD_BOUND]);; + +(* ------------------------------------------------------------------------- *) +(* The GHASH polynomial p(x) = x^128 + x^7 + x^2 + x + 1 *) +(* ------------------------------------------------------------------------- *) + +let ghash_poly = define + `ghash_poly = + ring_sum bool_poly {128,7,2,1,0} + (\i. ring_pow bool_poly (poly_var bool_ring one) i)`;; + +let GHASH_BOOL_POLY = prove + (`ghash_poly IN ring_carrier bool_poly`, + REWRITE_TAC[ghash_poly; RING_SUM]);; + +let RING_POLYNOMIAL_GHASH_POLY = prove + (`ring_polynomial bool_ring ghash_poly`, + REWRITE_TAC[RING_POLYNOMIAL; GSYM bool_poly; GHASH_BOOL_POLY]);; + +let GHASH_POLY_OF_WORD = prove + (`128 < dimindex(:N) + ==> ghash_poly = + poly_of_word(word 0x100000000000000000000000000000087:N word)`, + REPEAT STRIP_TAC THEN REWRITE_TAC[ghash_poly] THEN + SIMP_TAC[RING_SUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY; + IN_INSERT; ARITH_EQ; NOT_IN_EMPTY] THEN + REWRITE_TAC[POLY_VARPOW_BOOL_POLY] THEN + REWRITE_TAC[bool_poly; POLY_RING_VAR_POW_1] THEN + REWRITE_TAC[POLY_RING; poly_add; POLY_0; poly_of_word] THEN + GEN_REWRITE_TAC I [FUN_EQ_THM] THEN + REWRITE_TAC[FORALL_FUN_FROM_1] THEN + REWRITE_TAC[FUN_EQ_THM; BOOL_RING] THEN + X_GEN_TAC `i:num` THEN ASM_CASES_TAC `i < 129` THENL + [POP_ASSUM MP_TAC THEN SPEC_TAC(`i:num`,`i:num`) THEN + CONV_TAC EXPAND_CASES_CONV THEN + REWRITE_TAC[BIT_WORD] THEN CONV_TAC NUM_REDUCE_CONV THEN + ASM_ARITH_TAC; + ALL_TAC] THEN + TRANS_TAC EQ_TRANS `F` THEN CONJ_TAC THENL + [REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN ASM_ARITH_TAC; + REWRITE_TAC[BIT_WORD]] THEN + MATCH_MP_TAC(MESON[ODD] `n = 0 ==> ~(p /\ ODD n)`) THEN + SIMP_TAC[DIV_EQ_0; ARITH_EQ; EXP_EQ_0] THEN + TRANS_TAC LTE_TRANS `2 EXP 129` THEN REWRITE_TAC[LE_EXP] THEN + ASM_ARITH_TAC);; + +let POLY_DEG_GHASH_POLY = prove + (`poly_deg bool_ring ghash_poly = 128`, + MP_TAC(INST_TYPE [`:129`,`:N`] GHASH_POLY_OF_WORD) THEN + CONV_TAC(ONCE_DEPTH_CONV DIMINDEX_CONV) THEN + CONV_TAC NUM_REDUCE_CONV THEN DISCH_THEN SUBST1_TAC THEN + REWRITE_TAC[POLY_DEG_POLY_OF_WORD] THEN + CONV_TAC(ONCE_DEPTH_CONV DIMINDEX_CONV) THEN + CONV_TAC WORD_REDUCE_CONV THEN CONV_TAC NUM_REDUCE_CONV);; + +(* ------------------------------------------------------------------------- *) +(* Equivalence modulo the ghash polynomial, and reduction at word level *) +(* ------------------------------------------------------------------------- *) + +let mod_ghash = define + `mod_ghash p q <=> + p IN ring_carrier bool_poly /\ q IN ring_carrier bool_poly /\ + ring_sub bool_poly p q IN ideal_generated bool_poly {ghash_poly}`;; + +let MOD_GHASH_0 = prove + (`!p. (p == ring_0 bool_poly) (mod_ghash) <=> + ring_divides bool_poly ghash_poly p`, + GEN_TAC THEN REWRITE_TAC[mod_ghash; cong; ring_divides] THEN + ASM_CASES_TAC `p IN ring_carrier bool_poly` THEN + ASM_SIMP_TAC[IN_IDEAL_GENERATED_SING_EQ; RING_SUB_RZERO; GHASH_BOOL_POLY; + ring_divides; RING_0]);; + +let MOD_GHASH_REFL = prove + (`!p. (p == p) (mod_ghash) <=> p IN ring_carrier bool_poly`, + GEN_TAC THEN REWRITE_TAC[cong; mod_ghash] THEN + ASM_CASES_TAC `p IN ring_carrier bool_poly` THEN + ASM_SIMP_TAC[RING_SUB_REFL; IN_RING_IDEAL_0; RING_IDEAL_IDEAL_GENERATED]);; + +let MOD_GHASH_REFL_GEN = prove + (`!p q. p IN ring_carrier bool_poly /\ q = p ==> (p == q) (mod_ghash)`, + MESON_TAC[MOD_GHASH_REFL]);; + +let MOD_GHASH_SYM = prove + (`!p q. (p == q) (mod_ghash) <=> (q == p) (mod_ghash)`, + REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC + [`p IN ring_carrier bool_poly`; `q IN ring_carrier bool_poly`] THEN + ASM_REWRITE_TAC[cong; mod_ghash] THEN + ASM_MESON_TAC[IN_RING_IDEAL_NEG; RING_IDEAL_IDEAL_GENERATED; + RING_RULE `ring_neg r (ring_sub r a b) = ring_sub r b a`]);; + +let MOD_GHASH_TRANS = prove + (`!p q r. + (p == q) (mod_ghash) /\ (q == r) (mod_ghash) ==> (p == r) (mod_ghash)`, + REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC + [`p IN ring_carrier bool_poly`; `q IN ring_carrier bool_poly`; + `r IN ring_carrier bool_poly`] THEN + ASM_REWRITE_TAC[cong; mod_ghash] THEN + ASM_MESON_TAC[IN_RING_IDEAL_ADD; RING_IDEAL_IDEAL_GENERATED; RING_RULE + `ring_add r (ring_sub r a b) (ring_sub r b c) = ring_sub r a c`]);; + +let MOD_GHASH_ADD = prove + (`!p p' q q'. + (p == p') (mod_ghash) /\ (q == q') (mod_ghash) + ==> (ring_add bool_poly p q == ring_add bool_poly p' q') (mod_ghash)`, + REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC + [`p IN ring_carrier bool_poly`; `p' IN ring_carrier bool_poly`; + `q IN ring_carrier bool_poly`; `q' IN ring_carrier bool_poly`] THEN + ASM_SIMP_TAC[cong; mod_ghash; RING_ADD] THEN + ASM_MESON_TAC[IN_RING_IDEAL_ADD; RING_IDEAL_IDEAL_GENERATED; RING_RULE + `ring_add r (ring_sub r p p') (ring_sub r q q') = + ring_sub r (ring_add r p q) (ring_add r p' q')`]);; + +let MOD_GHASH_SUB = prove + (`!p p' q q'. + (p == p') (mod_ghash) /\ (q == q') (mod_ghash) + ==> (ring_sub bool_poly p q == ring_sub bool_poly p' q') (mod_ghash)`, + REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC + [`p IN ring_carrier bool_poly`; `p' IN ring_carrier bool_poly`; + `q IN ring_carrier bool_poly`; `q' IN ring_carrier bool_poly`] THEN + ASM_SIMP_TAC[cong; mod_ghash; RING_SUB] THEN + ASM_MESON_TAC[IN_RING_IDEAL_SUB; RING_IDEAL_IDEAL_GENERATED; RING_RULE + `ring_sub r (ring_sub r p p') (ring_sub r q q') = + ring_sub r (ring_sub r p q) (ring_sub r p' q')`]);; + +let MOD_GHASH_MUL = prove + (`!p p' q q'. + (p == p') (mod_ghash) /\ (q == q') (mod_ghash) + ==> (ring_mul bool_poly p q == ring_mul bool_poly p' q') (mod_ghash)`, + REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC + [`p IN ring_carrier bool_poly`; `p' IN ring_carrier bool_poly`; + `q IN ring_carrier bool_poly`; `q' IN ring_carrier bool_poly`] THEN + ASM_SIMP_TAC[cong; mod_ghash; RING_MUL] THEN + ASM_MESON_TAC[IN_RING_IDEAL_ADD; IN_RING_IDEAL_LMUL; + RING_IDEAL_IDEAL_GENERATED; RING_RULE + `ring_add r (ring_mul r q (ring_sub r p p')) + (ring_mul r p' (ring_sub r q q')) = + ring_sub r (ring_mul r p q) (ring_mul r p' q')`]);; + +let ghash_reduce1 = define + `ghash_reduce1 (x:N word) = + word_xor (word_subword x (0,128):N word) + (word_pmul (word_ushr x 128) (word 0x87:N word))`;; + +let GHASH_REDUCE1 = prove + (`!x:N word. + ghash_reduce1 x = + word_xor (word_subword x (0,128)) + (word_xor (word_shl (word_ushr x 128) 7) + (word_xor (word_shl (word_ushr x 128) 2) + (word_xor (word_shl (word_ushr x 128) 1) + (word_ushr x 128))))`, + let lemma = prove + (`word 0x87:N word = word_zx(word 0x87:byte)`, + REWRITE_TAC[word_zx] THEN CONV_TAC WORD_REDUCE_CONV) in + GEN_TAC THEN REWRITE_TAC[ghash_reduce1] THEN + ONCE_REWRITE_TAC[WORD_PMUL_SYM] THEN + REWRITE_TAC[WORD_EQ_BITS_ALT] THEN + X_GEN_TAC `i:num` THEN DISCH_TAC THEN + ONCE_REWRITE_TAC[lemma] THEN + ASM_REWRITE_TAC[BIT_WORD_XOR_ALT; BIT_WORD_PMUL] THEN + ASM_REWRITE_TAC[BIT_WORD_SHL; BIT_WORD_USHR] THEN + AP_TERM_TAC THEN AP_TERM_TAC THEN + REWRITE_TAC[BIT_WORD_ZX; BIT_WORD; DIMINDEX_8] THEN + REWRITE_TAC[GSYM BITVAL_AND; GSYM CONJ_ASSOC] THEN + ONCE_REWRITE_TAC[TAUT `p /\ q /\ r <=> q /\ p /\ r`] THEN + REWRITE_TAC[bitval] THEN ONCE_REWRITE_TAC[MESON[] + `(if p /\ q then a else b) = if p then (if q then a else b) else b`] THEN + ONCE_REWRITE_TAC[GSYM NSUM_RESTRICT_SET] THEN + ONCE_REWRITE_TAC[SET_RULE + `{i | i IN s /\ P i} = {i | i IN {j | P j} /\ i IN s}`] THEN + REWRITE_TAC[NSUM_RESTRICT_SET] THEN + REWRITE_TAC[NUMSEG_LT; ARITH; IN_NUMSEG; LE_0] THEN + CONV_TAC(ONCE_DEPTH_CONV EXPAND_NSUM_CONV) THEN + CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[COND_ID; ADD_CLAUSES] THEN + REWRITE_TAC[MESON[] + `(if p then (if q then a else b) else b) = (if p /\ q then a else b)`] THEN + REWRITE_TAC[GSYM bitval; ODD_ADD; ODD_BITVAL] THEN + REWRITE_TAC[CONJ_ASSOC] THEN + ASM_SIMP_TAC[ARITH_RULE `i:num < N ==> (a <= i /\ a < N <=> a <= i)`] THEN + REWRITE_TAC[ADD_CLAUSES; SUB_0; LE_0] THEN CONV_TAC TAUT);; + +let POLY_EQUIV_GHASH_REDUCE1 = prove + (`!x:N word. (poly_of_word(ghash_reduce1 x) == poly_of_word x) (mod_ghash)`, + let lemma = prove + (`!x:N word. + word_subword x (0,128) = + word_xor x (word_shl (word_ushr x 128) 128)`, + GEN_TAC THEN ONCE_REWRITE_TAC[WORD_EQ_BITS_ALT] THEN + SIMP_TAC[BIT_WORD_SUBWORD; BIT_WORD_XOR; BIT_WORD_SHL; BIT_WORD_USHR] THEN + SIMP_TAC[ADD_CLAUSES; ARITH_RULE `i < MIN a b <=> i < a /\ i < b`] THEN + X_GEN_TAC `i:num` THEN DISCH_TAC THEN + ASM_CASES_TAC `128 <= i` THEN ASM_SIMP_TAC[GSYM NOT_LE; SUB_ADD]) in + GEN_TAC THEN REWRITE_TAC[cong; mod_ghash; BOOL_POLY_OF_WORD] THEN + SIMP_TAC[IDEAL_GENERATED_SING; GHASH_BOOL_POLY; IN_ELIM_THM] THEN + REWRITE_TAC[ring_divides; GHASH_BOOL_POLY] THEN + SIMP_TAC[RING_SUB; BOOL_POLY_OF_WORD] THEN + EXISTS_TAC `poly_of_word(word_ushr x 128:N word)` THEN + REWRITE_TAC[BOOL_POLY_OF_WORD] THEN + REWRITE_TAC[ghash_reduce1; lemma] THEN + REWRITE_TAC[BOOL_POLY_SUB; GSYM POLY_OF_WORD_XOR] THEN + REWRITE_TAC[WORD_BITWISE_RULE + `word_xor (word_xor (word_xor x a) b) x = word_xor a b`] THEN + ASM_CASES_TAC `word_ushr x 128:N word = word 0` THENL + [ASM_REWRITE_TAC[POLY_OF_WORD_0; WORD_PMUL_0; WORD_SHL_0; WORD_XOR_0] THEN + SIMP_TAC[RING_MUL_RZERO; GHASH_BOOL_POLY]; + ALL_TAC] THEN + SUBGOAL_THEN `128 < dimindex(:N)` MP_TAC THENL + [POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN + REWRITE_TAC[NOT_LT; WORD_USHR_EQ_0] THEN DISCH_TAC THEN + TRANS_TAC LTE_TRANS `2 EXP dimindex(:N)` THEN + REWRITE_TAC[VAL_BOUND; LE_EXP] THEN ASM_ARITH_TAC; + POP_ASSUM(K ALL_TAC) THEN DISCH_TAC] THEN + REWRITE_TAC[GSYM(CONJUNCT2 WORD_PMUL_POW2)] THEN + REWRITE_TAC[GSYM(CONJUNCT2 WORD_PMUL_XOR)] THEN + GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [WORD_PMUL_SYM] THEN + MP_TAC(ISPECL [`word(2 EXP 128):N word`; `word 0x87:N word`] + WORD_ADD_XOR) THEN + REWRITE_TAC[WORD_AND_POW2; BIT_WORD] THEN + CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[BITVAL_CLAUSES; MULT_CLAUSES] THEN + DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[GSYM WORD_ADD] THEN + CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[WORD_PMUL_POLY] THEN + ASM_SIMP_TAC[GSYM GHASH_POLY_OF_WORD] THEN + MATCH_MP_TAC POLY_OF_WORD_OF_POLY THEN + SIMP_TAC[RING_MUL; GHASH_BOOL_POLY; BOOL_POLY_OF_WORD] THEN + REWRITE_TAC[bool_poly; POLY_RING] THEN + W(MP_TAC o PART_MATCH (lhand o rand) POLY_DEG_MUL_LE o lhand o snd) THEN + REWRITE_TAC[RING_POLYNOMIAL_GHASH_POLY; POLY_DEG_GHASH_POLY; + POLY_DEG_POLY_OF_WORD; RING_POLYNOMIAL_OF_WORD] THEN + MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] LET_TRANS) THEN + MATCH_MP_TAC(ARITH_RULE `128 < n /\ 128 <= c ==> 128 + n - 1 - c < n`) THEN + ASM_SIMP_TAC[WORD_LE_CLZ; LT_IMP_LE; BIT_WORD_USHR] THEN + MESON_TAC[BIT_GUARD]);; + +(* ------------------------------------------------------------------------- *) +(* Fixed-size eduction from 256 to 128 bits: 2 rounds of simple reduction. *) +(* ------------------------------------------------------------------------- *) + +let ghash_reduce = define + `(ghash_reduce:256 word -> 128 word) x = + word_zx(ghash_reduce1(ghash_reduce1 x))`;; + +let POLY_EQUIV_GHASH_REDUCE = prove + (`!x. (poly_of_word(ghash_reduce x) == poly_of_word x) (mod_ghash)`, + GEN_TAC THEN + MP_TAC(ISPEC `x:256 word` POLY_EQUIV_GHASH_REDUCE1) THEN + MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] MOD_GHASH_TRANS) THEN + MP_TAC(ISPEC `ghash_reduce1 x:256 word` POLY_EQUIV_GHASH_REDUCE1) THEN + MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] MOD_GHASH_TRANS) THEN + REWRITE_TAC[ghash_reduce; GSYM WORD_OF_POLY_OF_WORD_GEN] THEN + MATCH_MP_TAC MOD_GHASH_REFL_GEN THEN REWRITE_TAC[BOOL_POLY_OF_WORD] THEN + CONV_TAC SYM_CONV THEN MATCH_MP_TAC POLY_OF_WORD_OF_POLY THEN + REWRITE_TAC[BOOL_POLY_OF_WORD; POLY_DEG_POLY_OF_WORD] THEN + CONV_TAC(ONCE_DEPTH_CONV DIMINDEX_CONV) THEN + MATCH_MP_TAC(ARITH_RULE `128 <= a ==> 256 - 1 - a < 128`) THEN + REWRITE_TAC[WORD_LE_CLZ] THEN ONCE_REWRITE_TAC[BIT_GUARD] THEN + CONV_TAC(ONCE_DEPTH_CONV DIMINDEX_CONV) THEN + CONV_TAC NUM_REDUCE_CONV THEN + REWRITE_TAC[TAUT `p /\ q ==> r <=> p ==> ~r ==> ~q`] THEN + REWRITE_TAC[GHASH_REDUCE1] THEN + CONV_TAC EXPAND_CASES_CONV THEN + CONV_TAC(TOP_DEPTH_CONV BIT_WORD_CONV) THEN + CONV_TAC NUM_REDUCE_CONV);; + +(* ------------------------------------------------------------------------- *) +(* Some explicit computations of high powers of X. *) +(* ------------------------------------------------------------------------- *) + +let [X_POWPOW_128; X_POWPOW_64] = + let base = prove + (`(ring_pow bool_poly (poly_var bool_ring one) (2 EXP 0) == + poly_of_word(word 0x2:int128)) (mod_ghash)`, + MATCH_MP_TAC MOD_GHASH_REFL_GEN THEN + REWRITE_TAC[POLY_VARPOW_BOOL_POLY] THEN + REWRITE_TAC[EXP; POLY_RING_VAR_POW_1; bool_poly] THEN + REWRITE_TAC[poly_of_word] THEN + GEN_REWRITE_TAC I [FUN_EQ_THM] THEN + GEN_REWRITE_TAC I [FORALL_FUN_FROM_1] THEN + X_GEN_TAC `k:num` THEN REWRITE_TAC[] THEN + REWRITE_TAC[MESON[] `(\x:1. a) = (\x. b) <=> a = b`] THEN + REWRITE_TAC[BOOL_RING; MESON[] `(if p then T else F) <=> p`] THEN + REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC + (ARITH_RULE `k = 0 \/ k = 1 \/ 2 <= k`) THEN + ASM_REWRITE_TAC[] THEN CONV_TAC WORD_REDUCE_CONV THEN + CONV_TAC NUM_REDUCE_CONV THEN + MATCH_MP_TAC(TAUT `~q /\ ~p ==> (p <=> q)`) THEN + CONJ_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[BIT_WORD]] THEN + UNDISCH_TAC `2 <= k` THEN + REWRITE_TAC[TAUT `r ==> ~(p /\ q) <=> p ==> r ==> ~q`] THEN + CONV_TAC(ONCE_DEPTH_CONV DIMINDEX_CONV) THEN + SPEC_TAC(`k:num`,`k:num`) THEN CONV_TAC EXPAND_CASES_CONV THEN + CONV_TAC NUM_REDUCE_CONV) + and step = prove + (`!(x:int128) n. + (ring_pow bool_poly (poly_var bool_ring one) (2 EXP n) == + poly_of_word x) (mod_ghash) + ==> (ring_pow bool_poly (poly_var bool_ring one) (2 EXP SUC n) == + poly_of_word(ghash_reduce(word_pmul x x))) (mod_ghash)`, + REPEAT GEN_TAC THEN + DISCH_THEN(MP_TAC o MATCH_MP MOD_GHASH_MUL o W CONJ) THEN + SIMP_TAC[GSYM RING_POW_2; POLY_VARPOW_BOOL_POLY] THEN + SIMP_TAC[RING_POW_POW; POLY_VAR_BOOL_POLY] THEN + REWRITE_TAC[EXP; MULT_SYM] THEN + MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] MOD_GHASH_TRANS) THEN + REWRITE_TAC[GSYM POLY_OF_WORD_PMUL_2N] THEN + ONCE_REWRITE_TAC[MOD_GHASH_SYM] THEN + REWRITE_TAC[POLY_EQUIV_GHASH_REDUCE]) in + let rec rules n = + if n = 0 then [base] else + let lis = rules(n - 1) in + let th1 = MATCH_MP step (hd lis) in + let th2 = CONV_RULE(RATOR_CONV(BINOP2_CONV + (RAND_CONV(RAND_CONV NUM_SUC_CONV)) + (ONCE_DEPTH_CONV WORD_PMUL_CONV THENC + REWRITE_CONV[ghash_reduce; ghash_reduce1] THENC + DEPTH_CONV(WORD_RED_CONV ORELSEC WORD_PMUL_CONV)))) th1 in + th2::lis in + let lis = rev(rules 128) in + let th_0 = SIMP_RULE[EXP; RING_POW_1; POLY_VAR_BOOL_POLY] (el 0 lis) + and th_64 = el 64 lis + and th_128 = el 128 lis in + map + (REWRITE_RULE[GSYM BOOL_POLY_SUB; POLY_OF_WORD_0] o + CONV_RULE WORD_REDUCE_CONV o + REWRITE_RULE[GSYM POLY_OF_WORD_XOR; BOOL_POLY_SUB]) + [MATCH_MP MOD_GHASH_SUB (CONJ th_128 th_0); + MATCH_MP MOD_GHASH_SUB (CONJ th_64 th_0)];; + +(* ------------------------------------------------------------------------- *) +(* Now use the Rabin test to prove irreducibility. *) +(* ------------------------------------------------------------------------- *) + +let FINITE_BOOL_RING = prove + (`FINITE(ring_carrier bool_ring)`, + REWRITE_TAC[BOOL_RING; FINITE_BOOL]);; + +let CARD_BOOL_RING = prove + (`CARD(ring_carrier bool_ring) = 2`, + REWRITE_TAC[BOOL_RING; CARD_BOOL]);; + +let BEZOUT_BOOL_POLY = prove + (`bezout_ring bool_poly`, + REWRITE_TAC[bool_poly] THEN + MESON_TAC[PID_EQ_UFD_BEZOUT_RING; PID_POLY_RING; FIELD_BOOL_RING]);; + +let RING_IRREDUCBLE_GHASH_POLYNOMIAL = prove + (`ring_irreducible bool_poly ghash_poly`, + let lemma = prove + (`!s t. s IN ring_carrier bool_poly /\ + t IN ring_carrier bool_poly /\ + ring_add bool_poly (ring_mul bool_poly s ghash_poly) + (ring_mul bool_poly t p') = + ring_1 bool_poly + ==> (p == p') (mod_ghash) ==> ring_coprime bool_poly (ghash_poly,p)`, + REPEAT GEN_TAC THEN STRIP_TAC THEN + SIMP_TAC[cong; mod_ghash; IN_IDEAL_GENERATED_SING_EQ; GHASH_BOOL_POLY] THEN + STRIP_TAC THEN + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ring_divides]) THEN + ASM_SIMP_TAC[RING_SUB; IMP_CONJ; LEFT_IMP_EXISTS_THM] THEN + DISCH_TAC THEN X_GEN_TAC `d:(1->num)->bool` THEN REPEAT STRIP_TAC THEN + ASM_SIMP_TAC[BEZOUT_RING_COPRIME; BEZOUT_BOOL_POLY] THEN + EXISTS_TAC `ring_sub bool_poly s (ring_mul bool_poly t d)` THEN + EXISTS_TAC `t:(1->num)->bool` THEN + ASM_SIMP_TAC[RING_SUB; RING_MUL] THEN + REPEAT(POP_ASSUM MP_TAC) THEN + SPEC_TAC(`bool_poly`,`r:((1->num)->bool)ring`) THEN + RING_TAC) in + REWRITE_TAC[bool_poly] THEN MATCH_MP_TAC RABIN_IRREDUCIBILITY_SUFFICIENT THEN + EXISTS_TAC `128` THEN REWRITE_TAC[POLY_DEG_GHASH_POLY] THEN + REWRITE_TAC[FIELD_BOOL_RING; FINITE_BOOL_RING; CARD_BOOL_RING] THEN + REWRITE_TAC[GSYM bool_poly; GHASH_BOOL_POLY] THEN CONJ_TAC THENL + [DISCH_THEN(MP_TAC o AP_TERM + `poly_deg bool_ring:((1->num)->bool)->num`) THEN + REWRITE_TAC[POLY_DEG_GHASH_POLY] THEN + REWRITE_TAC[bool_poly; POLY_RING; POLY_DEG_0; ARITH_EQ]; + REWRITE_TAC[ARITH_EQ] THEN + REWRITE_TAC[GSYM(NUM_REDUCE_CONV `2 EXP 7`)]] THEN + SIMP_TAC[IMP_CONJ; PRIME_DIVEXP_EQ] THEN + SIMP_TAC[DIVIDES_PRIME_PRIME; PRIME_2; ARITH_EQ] THEN + ONCE_REWRITE_TAC[TAUT `p ==> q ==> r <=> q ==> p ==> r`] THEN + REWRITE_TAC[FORALL_UNWIND_THM2; PRIME_2] THEN + CONV_TAC(ONCE_DEPTH_CONV NUM_EXP_CONV) THEN + CONV_TAC(ONCE_DEPTH_CONV NUM_DIV_CONV) THEN + REWRITE_TAC[GSYM MOD_GHASH_0; X_POWPOW_128] THEN + MP_TAC X_POWPOW_64 THEN MATCH_MP_TAC lemma THEN + MAP_EVERY EXISTS_TAC + [`poly_of_word(word 0x34f319a5fb685836214ec51f73e3547b:129 word)`; + `poly_of_word(word 0x9e4af928ddbc838a41a8cafd2c95b018:129 word)`] THEN + REWRITE_TAC[BOOL_POLY_OF_WORD] THEN + MP_TAC(INST_TYPE [`:129`,`:N`] GHASH_POLY_OF_WORD) THEN + MP_TAC(INST_TYPE [`:128`,`:M`; `:129`,`:N`] POLY_OF_WORD_ZX) THEN + CONV_TAC(ONCE_DEPTH_CONV DIMINDEX_CONV) THEN CONV_TAC NUM_REDUCE_CONV THEN + DISCH_THEN(fun th -> ONCE_REWRITE_TAC[GSYM th]) THEN + DISCH_THEN SUBST1_TAC THEN CONV_TAC(ONCE_DEPTH_CONV WORD_ZX_CONV) THEN + REWRITE_TAC[GSYM POLY_OF_WORD_PMUL_2N; GSYM POLY_OF_WORD_XOR] THEN + CONV_TAC(DEPTH_CONV(WORD_PMUL_CONV ORELSEC WORD_RED_CONV)) THEN + REWRITE_TAC[POLY_OF_WORD_1]);; From 9aa96c473063275eeeda065f6db89970ea4ea614 Mon Sep 17 00:00:00 2001 From: sanketh Date: Wed, 8 Apr 2026 19:32:41 +0000 Subject: [PATCH 6/7] Add GCM spec (SP 800-38D) with KATs common/gcm.ml: High-level GCM spec close to NIST SP 800-38D: - gf128_mul (via word_pmul + ghash_reduce), ghash, inc32, gctr, gcm_ae (Algorithm 4), gcm_ad (Algorithm 5). - Simplified to 96-bit IV, full 128-bit blocks, 128-bit tag. - KATs: inc32, GCTR, gf128_mul, GHASH, plus GCM-AE/AD for TC1-TC3 from the GCM revised spec (McGrew & Viega, Appendix B). --- common/gcm.ml | 398 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 398 insertions(+) create mode 100644 common/gcm.ml diff --git a/common/gcm.ml b/common/gcm.ml new file mode 100644 index 000000000..8ec43bb16 --- /dev/null +++ b/common/gcm.ml @@ -0,0 +1,398 @@ +(* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0 + *) + +(* ========================================================================= *) +(* GCM definitions per NIST SP 800-38D. *) +(* *) +(* This file defines GCTR (Algorithm 3) and supporting functions. *) +(* AES cipher comes from common/fips197.ml. *) +(* ========================================================================= *) + +needs "common/fips197.ml";; +needs "common/ghash.ml";; + +(* ========================================================================= *) +(* inc32: increment the rightmost 32 bits of a 128-bit block (SP 800-38D *) +(* Section 6.2). The leftmost 96 bits are unchanged. *) +(* ========================================================================= *) + +let inc32 = new_definition + `inc32 (cb:128 word) : 128 word = + let top96:96 word = word_subword cb (32,96) in + let bot32:32 word = word_subword cb (0,32) in + word_join top96 (word_add bot32 (word 1 : 32 word)) : 128 word`;; + +let INC32_CONV = + REWRITE_CONV [inc32] THENC + TOP_DEPTH_CONV let_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV);; + +prove(`inc32 (word 0x00000000000000000000000000000001 : 128 word) = + word 0x00000000000000000000000000000002`, + CONV_TAC(LAND_CONV INC32_CONV) THEN REFL_TAC);; + +prove(`inc32 (word 0xCAFEBABE00000000DECAF00000000001 : 128 word) = + word 0xCAFEBABE00000000DECAF00000000002`, + CONV_TAC(LAND_CONV INC32_CONV) THEN REFL_TAC);; + +prove(`inc32 (word 0x00000000000000000000000FFFFFFFFF : 128 word) = + word 0x00000000000000000000000F00000000`, + CONV_TAC(LAND_CONV INC32_CONV) THEN REFL_TAC);; + +prove(`inc32 (word 0xFEEDFACEDEADBEEFFEEDFACEFFFFFFFF : 128 word) = + word 0xFEEDFACEDEADBEEFFEEDFACE00000000`, + CONV_TAC(LAND_CONV INC32_CONV) THEN REFL_TAC);; + +(* ========================================================================= *) +(* GCTR: NIST SP 800-38D Algorithm 3 (counter-mode encryption). *) +(* *) +(* Operates on full 128-bit blocks. Partial last block handling is deferred *) +(* to the GCM-AE/AD layer. Uses AES-128 cipher from fips197.ml. *) +(* ========================================================================= *) + +let gctr = define + `gctr (ks:(128 word) list) (icb:128 word) ([] : (128 word) list) = + ([] : (128 word) list) /\ + gctr ks icb (CONS x rest) = + CONS (word_xor x (aes128_cipher icb ks)) (gctr ks (inc32 icb) rest)`;; + +(* GCTR_CONV: evaluate gctr on concrete values, one block at a time. + Takes a key schedule definition theorem as argument. *) +let GCTR_STEP_CONV ks_def = + ONCE_REWRITE_CONV [gctr] THENC + REWRITE_CONV [ks_def] THENC + ONCE_DEPTH_CONV (FIPS197_ENCRYPT_CONV aes128_cipher ks_def) THENC + DEPTH_CONV WORD_RED_CONV THENC + ONCE_DEPTH_CONV (REWRITE_CONV [inc32] THENC + TOP_DEPTH_CONV let_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV));; + +let rec GCTR_CONV ks_def tm = + try + let th = GCTR_STEP_CONV ks_def tm in + let rhs = rand (concl th) in + (try let th2 = RAND_CONV (GCTR_CONV ks_def) rhs in TRANS th th2 + with _ -> th) + with _ -> REWRITE_CONV [gctr] tm;; + +(* Fast GCTR using precomputed AES tables from fips197.ml. *) +let GCTR_STEP_FAST_CONV ks_def = + ONCE_REWRITE_CONV [gctr] THENC + REWRITE_CONV [ks_def] THENC + ONCE_DEPTH_CONV (FIPS197_ENCRYPT_FAST_CONV aes128_cipher ks_def) THENC + DEPTH_CONV WORD_RED_CONV THENC + ONCE_DEPTH_CONV (REWRITE_CONV [inc32] THENC + TOP_DEPTH_CONV let_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV));; + +let rec GCTR_FAST_CONV ks_def tm = + try + let th = GCTR_STEP_FAST_CONV ks_def tm in + let rhs = rand (concl th) in + (try let th2 = RAND_CONV (GCTR_FAST_CONV ks_def) rhs in TRANS th th2 + with _ -> th) + with _ -> REWRITE_CONV [gctr] tm;; + +(* ========================================================================= *) +(* Key schedule for NIST SP 800-38D Test Case 3 (AES-128). *) +(* Key: 0xFEFFE9928665731C6D6A8F9467308308 *) +(* ========================================================================= *) + +let NIST_TC3_KEY_SCHEDULE = new_definition + `NIST_TC3_KEY_SCHEDULE : (128 word) list = + [ word 0xFEFFE9928665731C6D6A8F9467308308 + ; word 0xFB13D9177D76AA0B101C259F772CA697 + ; word 0x883751E2F541FBE9E55DDE76927178E1 + ; word 0x2F8BA9ADDACA52443F978C32ADE6F4D3 + ; word 0xA934CF3873FE9D7C4C69114EE18FE59D + ; word 0xCAED91C0B9130CBCF57A1DF214F5F86F + ; word 0x0CAC393AB5BF358640C528745430D01B + ; word 0x48DC961AFD63A39CBDA68BE8E9965BF3 + ; word 0x58E59B04A58638981820B370F1B6E883 + ; word 0x0D7E77A5A8F84F3DB0D8FC4D416E14CE + ; word 0xA484FC260C7CB31BBCA44F56FDCA5B98 + ]`;; + +(* ========================================================================= *) +(* GCTR KATs from NIST SP 800-38D Test Case 3. *) +(* Key: 0xFEFFE9928665731C6D6A8F9467308308 *) +(* ICB: 0xCAFEBABEFACEDBADDECAF88800000002 *) +(* ========================================================================= *) + +prove(`gctr AESAVS_ZERO_KEY_128_SCHEDULE + (word 0x00000000000000000000000000000002) + [word 0x00000000000000000000000000000000 : 128 word] = + [word 0x0388DACE60B6A392F328C2B971B2FE78]`, + CONV_TAC(LAND_CONV(GCTR_FAST_CONV AESAVS_ZERO_KEY_128_SCHEDULE)) THEN + REFL_TAC);; + +prove(`gctr NIST_TC3_KEY_SCHEDULE + (word 0xCAFEBABEFACEDBADDECAF88800000002) + [word 0xD9313225F88406E5A55909C5AFF5269A : 128 word] = + [word 0x42831EC2217774244B7221B784D0D49C]`, + CONV_TAC(LAND_CONV(GCTR_FAST_CONV NIST_TC3_KEY_SCHEDULE)) THEN + REFL_TAC);; + +prove(`gctr NIST_TC3_KEY_SCHEDULE + (word 0xCAFEBABEFACEDBADDECAF88800000002) + [ word 0xD9313225F88406E5A55909C5AFF5269A + ; word 0x86A7A9531534F7DA2E4C303D8A318A72 : 128 word] = + [ word 0x42831EC2217774244B7221B784D0D49C + ; word 0xE3AA212F2C02A4E035C17E2329ACA12E]`, + CONV_TAC(LAND_CONV(GCTR_FAST_CONV NIST_TC3_KEY_SCHEDULE)) THEN + REFL_TAC);; + +(* ========================================================================= *) +(* GF(2^128) multiplication: NIST SP 800-38D Section 6.3. *) +(* *) +(* Multiplication in GF(2^128) with irreducible polynomial *) +(* P(x) = x^128 + x^7 + x^2 + x + 1. *) +(* *) +(* NIST uses reflected bit ordering (bit 0 = MSB = coefficient of x^0). *) +(* We implement this as: bit-reverse inputs, carry-less multiply, reduce *) +(* mod P(x) using ghash_reduce from common/ghash.ml, then bit-reverse the *) +(* result. The reduction polynomial 0x87 = x^7+x^2+x+1 is the low part *) +(* of P(x). *) +(* ========================================================================= *) + +let bitrev128 = new_definition + `bitrev128 (x:128 word) : 128 word = word_reversefields 1 x`;; + +let gf128_mul = new_definition + `gf128_mul (X:128 word) (Y:128 word) : 128 word = + bitrev128 (ghash_reduce (word_pmul (bitrev128 X) (bitrev128 Y) : 256 word))`;; + +let GF128_MUL_CONV = + REWRITE_CONV [gf128_mul; bitrev128; ghash_reduce; ghash_reduce1] THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV) THENC + ONCE_DEPTH_CONV WORD_PMUL_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV) THENC + ONCE_DEPTH_CONV WORD_PMUL_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV) THENC + TRY_CONV(ONCE_DEPTH_CONV WORD_PMUL_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV));; + +prove(`gf128_mul (word 0x000000000000000000000000DEADBEEF) + (word 0x00000000000000000000000000000000 : 128 word) = + word 0x00000000000000000000000000000000`, + CONV_TAC(LAND_CONV GF128_MUL_CONV) THEN REFL_TAC);; + +prove(`gf128_mul (word 0x0388DACE60B6A392F328C2B971B2FE78) + (word 0x80000000000000000000000000000000 : 128 word) = + word 0x0388DACE60B6A392F328C2B971B2FE78`, + CONV_TAC(LAND_CONV GF128_MUL_CONV) THEN REFL_TAC);; + +prove(`gf128_mul (word 0x66E94BD4EF8A2C3B884CFA59CA342B2E) + (word 0x66E94BD4EF8A2C3B884CFA59CA342B2E : 128 word) = + word 0xA569901BB4B18906F5059D24465C904D`, + CONV_TAC(LAND_CONV GF128_MUL_CONV) THEN REFL_TAC);; + +prove(`gf128_mul (word 0x0388DACE60B6A392F328C2B971B2FE78) + (word 0x66E94BD4EF8A2C3B884CFA59CA342B2E : 128 word) = + word 0x5E2EC746917062882C85B0685353DEB7`, + CONV_TAC(LAND_CONV GF128_MUL_CONV) THEN REFL_TAC);; + +(* ========================================================================= *) +(* GHASH: NIST SP 800-38D Algorithm 2. *) +(* *) +(* GHASH(H, X_1 || ... || X_m) iterates gf128_mul: *) +(* Y_0 = 0, Y_i = gf128_mul(Y_{i-1} XOR X_i, H). *) +(* Takes an initial accumulator Y (normally word 0) for generality. *) +(* ========================================================================= *) + +let ghash = define + `ghash (H:128 word) (Y:128 word) ([] : (128 word) list) = Y /\ + ghash H Y (CONS x rest) = ghash H (gf128_mul (word_xor Y x) H) rest`;; + +(* Conversion for evaluating ghash on concrete values *) +let GHASH_STEP_CONV = + ONCE_REWRITE_CONV [ghash] THENC + DEPTH_CONV WORD_RED_CONV THENC + ONCE_DEPTH_CONV GF128_MUL_CONV;; + +let rec GHASH_CONV tm = + (GHASH_STEP_CONV THENC TRY_CONV GHASH_CONV) tm;; + +prove(`ghash (word 0x66E94BD4EF8A2C3B884CFA59CA342B2E) (word 0) + [word 0 : 128 word] = word 0`, + CONV_TAC(LAND_CONV GHASH_CONV) THEN REFL_TAC);; + +prove(`ghash (word 0x66E94BD4EF8A2C3B884CFA59CA342B2E) (word 0) + [word 0x0388DACE60B6A392F328C2B971B2FE78 : 128 word] = + word 0x5E2EC746917062882C85B0685353DEB7`, + CONV_TAC(LAND_CONV GHASH_CONV) THEN REFL_TAC);; + +prove(`ghash (word 0xB83B533708BF535D0AA6E52980D53B78) (word 0) + [ word 0x42831EC2217774244B7221B784D0D49C + ; word 0xE3AA212F2C02A4E035C17E2329ACA12E : 128 word] = + word 0xB714C9048389AFD9F9BC5C1D4378E052`, + CONV_TAC(LAND_CONV GHASH_CONV) THEN REFL_TAC);; + +(* ========================================================================= *) +(* GCM-AE: NIST SP 800-38D Algorithm 4 (authenticated encryption). *) +(* *) +(* Simplified to 96-bit IV, full 128-bit blocks, and 128-bit tag. *) +(* Key schedule is pre-expanded. Returns (ciphertext, tag). *) +(* ========================================================================= *) + +let gcm_ae = new_definition + `gcm_ae (ks:(128 word) list) (iv:96 word) + (P:(128 word) list) (A:(128 word) list) = + let H = aes128_cipher (word 0) ks in + let J0 : 128 word = word_join iv (word 1 : 32 word) in + let C = gctr ks (inc32 J0) P in + let len_block : 128 word = + word_join (word (128 * LENGTH A) : 64 word) + (word (128 * LENGTH C) : 64 word) in + let S = ghash H (word 0) (APPEND A (APPEND C [len_block])) in + let tag = word_xor S (aes128_cipher J0 ks) in + (C, tag)`;; + +(* ========================================================================= *) +(* GCM-AD: NIST SP 800-38D Algorithm 5 (authenticated decryption). *) +(* *) +(* Returns SOME plaintext if tag verifies, NONE otherwise. *) +(* ========================================================================= *) + +let gcm_ad = new_definition + `gcm_ad (ks:(128 word) list) (iv:96 word) + (C:(128 word) list) (A:(128 word) list) (tag:128 word) = + let H = aes128_cipher (word 0) ks in + let J0 : 128 word = word_join iv (word 1 : 32 word) in + let P = gctr ks (inc32 J0) C in + let len_block : 128 word = + word_join (word (128 * LENGTH A) : 64 word) + (word (128 * LENGTH C) : 64 word) in + let S = ghash H (word 0) (APPEND A (APPEND C [len_block])) in + let tag' = word_xor S (aes128_cipher J0 ks) in + if tag' = tag then SOME P else NONE`;; + + +(* ========================================================================= *) +(* KATs: NIST SP 800-38D Test Case 1 (AES-128, empty P, empty A, 96-bit IV) *) +(* Key: 0x00000000000000000000000000000000 *) +(* IV: 0x000000000000000000000000 *) +(* C: (empty) *) +(* T: 0x58e2fccefa7e3061367f1d57a4e7455a *) +(* ========================================================================= *) + +prove(`gcm_ae AESAVS_ZERO_KEY_128_SCHEDULE + (word 0 : 96 word) ([] : (128 word) list) ([] : (128 word) list) = + ([] : (128 word) list, + word 0x58e2fccefa7e3061367f1d57a4e7455a : 128 word)`, + CONV_TAC(REWRITE_CONV[gcm_ae; LET_DEF; LET_END_DEF]) THEN + CONV_TAC(ONCE_DEPTH_CONV(FIPS197_ENCRYPT_FAST_CONV aes128_cipher + AESAVS_ZERO_KEY_128_SCHEDULE)) THEN + CONV_TAC(REWRITE_CONV[gctr; inc32; LET_DEF; LET_END_DEF]) THEN + CONV_TAC(REWRITE_CONV[LENGTH; ARITH; APPEND]) THEN + CONV_TAC(DEPTH_CONV(WORD_RED_CONV ORELSEC NUM_RED_CONV)) THEN + CONV_TAC(REWRITE_CONV[ghash]) THEN + CONV_TAC(DEPTH_CONV WORD_RED_CONV) THEN + CONV_TAC(REWRITE_CONV[ghash]) THEN + CONV_TAC GF128_MUL_CONV THEN + CONV_TAC(ONCE_DEPTH_CONV(FIPS197_ENCRYPT_FAST_CONV aes128_cipher + AESAVS_ZERO_KEY_128_SCHEDULE)) THEN + CONV_TAC(DEPTH_CONV WORD_RED_CONV) THEN + REFL_TAC);; + +prove(`gcm_ad AESAVS_ZERO_KEY_128_SCHEDULE + (word 0 : 96 word) ([] : (128 word) list) ([] : (128 word) list) + (word 0x58e2fccefa7e3061367f1d57a4e7455a : 128 word) = + SOME ([] : (128 word) list)`, + CONV_TAC(REWRITE_CONV[gcm_ad; LET_DEF; LET_END_DEF]) THEN + CONV_TAC(ONCE_DEPTH_CONV(FIPS197_ENCRYPT_FAST_CONV aes128_cipher + AESAVS_ZERO_KEY_128_SCHEDULE)) THEN + CONV_TAC(REWRITE_CONV[gctr; inc32; LET_DEF; LET_END_DEF]) THEN + CONV_TAC(REWRITE_CONV[LENGTH; ARITH; APPEND]) THEN + CONV_TAC(DEPTH_CONV(WORD_RED_CONV ORELSEC NUM_RED_CONV)) THEN + CONV_TAC(REWRITE_CONV[ghash]) THEN + CONV_TAC(DEPTH_CONV WORD_RED_CONV) THEN + CONV_TAC(REWRITE_CONV[ghash]) THEN + CONV_TAC GF128_MUL_CONV THEN + CONV_TAC(ONCE_DEPTH_CONV(FIPS197_ENCRYPT_FAST_CONV aes128_cipher + AESAVS_ZERO_KEY_128_SCHEDULE)) THEN + CONV_TAC(DEPTH_CONV WORD_RED_CONV) THEN + REFL_TAC);; + +(* ========================================================================= *) +(* KATs: NIST SP 800-38D Test Case 2 (AES-128, 1-block P, empty A) *) +(* Key: 0x00000000000000000000000000000000 *) +(* IV: 0x000000000000000000000000 *) +(* P: 0x00000000000000000000000000000000 *) +(* C: 0x0388dace60b6a392f328c2b971b2fe78 *) +(* T: 0xab6e47d42cec13bdf53a67b21257bddf *) +(* Deconstructed KAT: each step proved individually (~45s total). *) +(* ========================================================================= *) + +let tc2_H = FIPS197_ENCRYPT_FAST_CONV aes128_cipher AESAVS_ZERO_KEY_128_SCHEDULE + `aes128_cipher (word 0 : 128 word) AESAVS_ZERO_KEY_128_SCHEDULE`;; + +let tc2_gctr = GCTR_FAST_CONV AESAVS_ZERO_KEY_128_SCHEDULE + `gctr AESAVS_ZERO_KEY_128_SCHEDULE (word 2 : 128 word) [word 0 : 128 word]`;; + +let tc2_gh0 = GHASH_STEP_CONV + `ghash (word 136792598789324718765670228683992083246) (word 0 : 128 word) + [word 4698274276341916077299333525606170232; word 128]`;; +let tc2_gh1 = CONV_RULE (RAND_CONV GHASH_STEP_CONV) tc2_gh0;; +let tc2_ghash = CONV_RULE (RAND_CONV (REWRITE_CONV [ghash])) tc2_gh1;; + +let tc2_aes_j0 = FIPS197_ENCRYPT_FAST_CONV aes128_cipher AESAVS_ZERO_KEY_128_SCHEDULE + `aes128_cipher (word 1 : 128 word) AESAVS_ZERO_KEY_128_SCHEDULE`;; + +let tc2_tag = WORD_RED_CONV + `word_xor (word 323733119472864005843474405660461955205 : 128 word) + (word 118150650284846871594443245464813258074 : 128 word)`;; +(* T = 0xab6e47d42cec13bdf53a67b21257bddf ✓ *) + +(* ========================================================================= *) +(* KATs: NIST SP 800-38D Test Case 3 (AES-128, 4-block P, empty A) *) +(* Key: 0xfeffe9928665731c6d6a8f9467308308 *) +(* IV: 0xcafebabefacedbaddecaf888 *) +(* P: d9313225...b16aedf5aa0de657ba637b391aafd255 (4 blocks) *) +(* C: 42831ec2...1ba30b396a0aac973d58e091473f5985 (4 blocks) *) +(* T: 0x4d5c2af327cd64a62cf35abd2ba6fab4 *) +(* Deconstructed KAT: each step proved individually (~100s total). *) +(* ========================================================================= *) + +let tc3_H = FIPS197_ENCRYPT_FAST_CONV aes128_cipher NIST_TC3_KEY_SCHEDULE + `aes128_cipher (word 0 : 128 word) NIST_TC3_KEY_SCHEDULE`;; + +let tc3_J0 = WORD_RED_CONV + `word_join ((word:num->96 word) 62823921025213631346103744648) + ((word:num->32 word) 1) : 128 word`;; + +let tc3_inc32_J0 = (REWRITE_CONV [inc32] THENC TOP_DEPTH_CONV let_CONV THENC + DEPTH_CONV (WORD_RED_CONV ORELSEC NUM_RED_CONV)) + `inc32 (word 269826686209779338044916040286295031809 : 128 word)`;; + +let tc3_gctr = GCTR_FAST_CONV NIST_TC3_KEY_SCHEDULE + `gctr NIST_TC3_KEY_SCHEDULE + (word 269826686209779338044916040286295031810 : 128 word) + [word 288697914760229039799526377950673184410; + word 178987099320277768797432184810360638066; + word 37530176933640231328893244680507405605; + word 235828565115539938141123428489895072341]`;; + +let tc3_gh0 = GHASH_STEP_CONV + `ghash (word 244885984539331295400417538152420686712) (word 0 : 128 word) + [word 88409862463181563309052745007072597148; + word 302618118565987919409388035474461597998; + word 44970902868695888635186260267724220933; + word 36735727929463124289467830015528753541; + word 512]`;; +let tc3_gh1 = CONV_RULE (RAND_CONV GHASH_STEP_CONV) tc3_gh0;; +let tc3_gh2 = CONV_RULE (RAND_CONV GHASH_STEP_CONV) tc3_gh1;; +let tc3_gh3 = CONV_RULE (RAND_CONV GHASH_STEP_CONV) tc3_gh2;; +let tc3_gh4 = CONV_RULE (RAND_CONV GHASH_STEP_CONV) tc3_gh3;; +let tc3_ghash = CONV_RULE (RAND_CONV (REWRITE_CONV [ghash])) tc3_gh4;; + +let tc3_aes_j0 = FIPS197_ENCRYPT_FAST_CONV aes128_cipher NIST_TC3_KEY_SCHEDULE + `aes128_cipher (word 269826686209779338044916040286295031809 : 128 word) + NIST_TC3_KEY_SCHEDULE`;; + +let tc3_tag = WORD_RED_CONV + `word_xor (word 168953176186840158469309092053489897132 : 128 word) + (word 66830545604809547225110084840681354264 : 128 word)`;; +(* T = 0x4d5c2af327cd64a62cf35abd2ba6fab4 ✓ *) \ No newline at end of file From 2f81c762c044ac6dd22a2b9fb5e43c498eb7b767 Mon Sep 17 00:00:00 2001 From: sanketh Date: Tue, 5 May 2026 15:34:34 +0000 Subject: [PATCH 7/7] whitespace --- common/fips197.ml | 6 +++--- common/gcm.ml | 44 ++++++++++++++++++++++---------------------- 2 files changed, 25 insertions(+), 25 deletions(-) diff --git a/common/fips197.ml b/common/fips197.ml index 93110d807..9f8f02844 100644 --- a/common/fips197.ml +++ b/common/fips197.ml @@ -374,12 +374,12 @@ let FIPS197_ENCRYPT_CONV cipher_def ks_def = FIPS197_FINAL_ROUND_REDUCE_CONV;; (* ========================================================================= *) -(* Fast AES conversions via precomputed lookup tables. *) +(* Fast AES conversions via precomputed lookup tables. *) (* *) (* The bottleneck in AES evaluation is word_subword on 2048-bit constants *) -(* (joined_GF2 for S-box, joined_FFmul_02/03 for MixColumns). *) +(* (joined_GF2 for S-box, joined_FFmul_02/03 for MixColumns). *) (* Precomputing all 256 entries for each table eliminates this bottleneck. *) -(* One-time cost: ~48s. Speedup: AES-128 from ~40s to ~7s per call. *) +(* One-time cost: ~48s. Speedup: AES-128 from ~40s to ~7s per call. *) (* ========================================================================= *) let aes_sbox_table = Array.init 256 (fun n -> diff --git a/common/gcm.ml b/common/gcm.ml index 8ec43bb16..ce82ba301 100644 --- a/common/gcm.ml +++ b/common/gcm.ml @@ -48,7 +48,7 @@ prove(`inc32 (word 0xFEEDFACEDEADBEEFFEEDFACEFFFFFFFF : 128 word) = (* ========================================================================= *) (* GCTR: NIST SP 800-38D Algorithm 3 (counter-mode encryption). *) (* *) -(* Operates on full 128-bit blocks. Partial last block handling is deferred *) +(* Operates on full 128-bit blocks. Partial last block handling is deferred *) (* to the GCM-AE/AD layer. Uses AES-128 cipher from fips197.ml. *) (* ========================================================================= *) @@ -97,7 +97,7 @@ let rec GCTR_FAST_CONV ks_def tm = (* ========================================================================= *) (* Key schedule for NIST SP 800-38D Test Case 3 (AES-128). *) -(* Key: 0xFEFFE9928665731C6D6A8F9467308308 *) +(* Key: 0xFEFFE9928665731C6D6A8F9467308308 *) (* ========================================================================= *) let NIST_TC3_KEY_SCHEDULE = new_definition @@ -116,9 +116,9 @@ let NIST_TC3_KEY_SCHEDULE = new_definition ]`;; (* ========================================================================= *) -(* GCTR KATs from NIST SP 800-38D Test Case 3. *) -(* Key: 0xFEFFE9928665731C6D6A8F9467308308 *) -(* ICB: 0xCAFEBABEFACEDBADDECAF88800000002 *) +(* GCTR KATs from NIST SP 800-38D Test Case 3. *) +(* Key: 0xFEFFE9928665731C6D6A8F9467308308 *) +(* ICB: 0xCAFEBABEFACEDBADDECAF88800000002 *) (* ========================================================================= *) prove(`gctr AESAVS_ZERO_KEY_128_SCHEDULE @@ -148,12 +148,12 @@ prove(`gctr NIST_TC3_KEY_SCHEDULE (* GF(2^128) multiplication: NIST SP 800-38D Section 6.3. *) (* *) (* Multiplication in GF(2^128) with irreducible polynomial *) -(* P(x) = x^128 + x^7 + x^2 + x + 1. *) +(* P(x) = x^128 + x^7 + x^2 + x + 1. *) (* *) (* NIST uses reflected bit ordering (bit 0 = MSB = coefficient of x^0). *) (* We implement this as: bit-reverse inputs, carry-less multiply, reduce *) -(* mod P(x) using ghash_reduce from common/ghash.ml, then bit-reverse the *) -(* result. The reduction polynomial 0x87 = x^7+x^2+x+1 is the low part *) +(* mod P(x) using ghash_reduce from common/ghash.ml, then bit-reverse the *) +(* result. The reduction polynomial 0x87 = x^7+x^2+x+1 is the low part *) (* of P(x). *) (* ========================================================================= *) @@ -198,8 +198,8 @@ prove(`gf128_mul (word 0x0388DACE60B6A392F328C2B971B2FE78) (* GHASH: NIST SP 800-38D Algorithm 2. *) (* *) (* GHASH(H, X_1 || ... || X_m) iterates gf128_mul: *) -(* Y_0 = 0, Y_i = gf128_mul(Y_{i-1} XOR X_i, H). *) -(* Takes an initial accumulator Y (normally word 0) for generality. *) +(* Y_0 = 0, Y_i = gf128_mul(Y_{i-1} XOR X_i, H). *) +(* Takes an initial accumulator Y (normally word 0) for generality. *) (* ========================================================================= *) let ghash = define @@ -231,7 +231,7 @@ prove(`ghash (word 0xB83B533708BF535D0AA6E52980D53B78) (word 0) CONV_TAC(LAND_CONV GHASH_CONV) THEN REFL_TAC);; (* ========================================================================= *) -(* GCM-AE: NIST SP 800-38D Algorithm 4 (authenticated encryption). *) +(* GCM-AE: NIST SP 800-38D Algorithm 4 (authenticated encryption). *) (* *) (* Simplified to 96-bit IV, full 128-bit blocks, and 128-bit tag. *) (* Key schedule is pre-expanded. Returns (ciphertext, tag). *) @@ -251,7 +251,7 @@ let gcm_ae = new_definition (C, tag)`;; (* ========================================================================= *) -(* GCM-AD: NIST SP 800-38D Algorithm 5 (authenticated decryption). *) +(* GCM-AD: NIST SP 800-38D Algorithm 5 (authenticated decryption). *) (* *) (* Returns SOME plaintext if tag verifies, NONE otherwise. *) (* ========================================================================= *) @@ -271,11 +271,11 @@ let gcm_ad = new_definition (* ========================================================================= *) -(* KATs: NIST SP 800-38D Test Case 1 (AES-128, empty P, empty A, 96-bit IV) *) +(* KATs: NIST SP 800-38D Test Case 1 (AES-128, empty P, empty A, 96-bit IV) *) (* Key: 0x00000000000000000000000000000000 *) (* IV: 0x000000000000000000000000 *) (* C: (empty) *) -(* T: 0x58e2fccefa7e3061367f1d57a4e7455a *) +(* T: 0x58e2fccefa7e3061367f1d57a4e7455a *) (* ========================================================================= *) prove(`gcm_ae AESAVS_ZERO_KEY_128_SCHEDULE @@ -317,12 +317,12 @@ prove(`gcm_ad AESAVS_ZERO_KEY_128_SCHEDULE REFL_TAC);; (* ========================================================================= *) -(* KATs: NIST SP 800-38D Test Case 2 (AES-128, 1-block P, empty A) *) +(* KATs: NIST SP 800-38D Test Case 2 (AES-128, 1-block P, empty A) *) (* Key: 0x00000000000000000000000000000000 *) (* IV: 0x000000000000000000000000 *) (* P: 0x00000000000000000000000000000000 *) -(* C: 0x0388dace60b6a392f328c2b971b2fe78 *) -(* T: 0xab6e47d42cec13bdf53a67b21257bddf *) +(* C: 0x0388dace60b6a392f328c2b971b2fe78 *) +(* T: 0xab6e47d42cec13bdf53a67b21257bddf *) (* Deconstructed KAT: each step proved individually (~45s total). *) (* ========================================================================= *) @@ -347,12 +347,12 @@ let tc2_tag = WORD_RED_CONV (* T = 0xab6e47d42cec13bdf53a67b21257bddf ✓ *) (* ========================================================================= *) -(* KATs: NIST SP 800-38D Test Case 3 (AES-128, 4-block P, empty A) *) -(* Key: 0xfeffe9928665731c6d6a8f9467308308 *) +(* KATs: NIST SP 800-38D Test Case 3 (AES-128, 4-block P, empty A) *) +(* Key: 0xfeffe9928665731c6d6a8f9467308308 *) (* IV: 0xcafebabefacedbaddecaf888 *) -(* P: d9313225...b16aedf5aa0de657ba637b391aafd255 (4 blocks) *) -(* C: 42831ec2...1ba30b396a0aac973d58e091473f5985 (4 blocks) *) -(* T: 0x4d5c2af327cd64a62cf35abd2ba6fab4 *) +(* P: d9313225...b16aedf5aa0de657ba637b391aafd255 (4 blocks) *) +(* C: 42831ec2...1ba30b396a0aac973d58e091473f5985 (4 blocks) *) +(* T: 0x4d5c2af327cd64a62cf35abd2ba6fab4 *) (* Deconstructed KAT: each step proved individually (~100s total). *) (* ========================================================================= *)