From fa2c26500b9827aa8a57a5de15d353bb7f46afaa Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Tue, 3 Dec 2024 11:14:25 +0000
Subject: [PATCH 01/27] Start looking at version of keccak operating on words

---
 examples/Crypto/Keccak/keccakScript.sml | 343 +++++++++++++++++++++++-
 1 file changed, 337 insertions(+), 6 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 45f61c5f67..271ac28ab4 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -1,8 +1,8 @@
-open HolKernel Parse boolLib bossLib dep_rewrite
+open HolKernel Parse boolLib bossLib dep_rewrite blastLib
      bitLib reduceLib combinLib optionLib sptreeLib wordsLib computeLib;
 open optionTheory pairTheory arithmeticTheory combinTheory listTheory
      rich_listTheory whileTheory bitTheory dividesTheory wordsTheory
-     logrootTheory sptreeTheory;
+     numposrepTheory logrootTheory sptreeTheory;
 
 (* The SHA-3 Standard: https://doi.org/10.6028/NIST.FIPS.202 *)
 
@@ -10,6 +10,211 @@ val _ = new_theory "keccak";
 
 val _ = numLib.temp_prefer_num();
 
+Theorem LENGTH_word_to_bin_list_bound:
+  LENGTH (word_to_bin_list (w:'a word)) <= (dimindex (:'a))
+Proof
+  rw[word_to_bin_list_def, wordsTheory.w2l_def, LENGTH_n2l]
+  \\ Cases_on`w` \\ simp[]
+  \\ fs[dimword_def, GSYM LESS_EQ, LOG2_def, LT_EXP_LOG]
+QED
+
+Theorem chunks_append_divides:
+  ∀n l1 l2.
+    0 < n /\ divides n (LENGTH l1) /\ ~NULL l1 /\ ~NULL l2 ==>
+    chunks n (l1 ++ l2) = chunks n l1 ++ chunks n l2
+Proof
+  recInduct chunks_ind
+  \\ rw[divides_def, PULL_EXISTS]
+  \\ simp[Once chunks_def]
+  \\ Cases_on`q=0` \\ gs[]
+  \\ IF_CASES_TAC
+  >- ( Cases_on`q` \\ gs[ADD1, LEFT_ADD_DISTRIB] \\ gs[LESS_OR_EQ] )
+  \\ simp[DROP_APPEND, TAKE_APPEND]
+  \\ qmatch_goalsub_abbrev_tac`lhs = _`
+  \\ simp[Once chunks_def]
+  \\ Cases_on`q = 1` \\ gs[]
+  >- (
+    simp[Abbr`lhs`]
+    \\ gs[NOT_LESS_EQUAL]
+    \\ simp[DROP_LENGTH_TOO_LONG])
+  \\ simp[Abbr`lhs`]
+  \\ `n - n * q = 0` by simp[]
+  \\ simp[]
+  \\ first_x_assum irule
+  \\ simp[NULL_EQ]
+  \\ qexists_tac`q - 1`
+  \\ simp[]
+QED
+
+Theorem chunks_length:
+  chunks (LENGTH ls) ls = [ls]
+Proof
+  rw[Once chunks_def]
+QED
+
+Theorem MEM_w2l_less:
+  1 < b /\ MEM x (w2l b w) ==> x < b
+Proof
+  Cases_on`w`
+  \\ rw[wordsTheory.w2l_def]
+  \\ rpt $ pop_assum mp_tac
+  \\ map_every qid_spec_tac [`x`,`n`,`b`]
+  \\ recInduct n2l_ind
+  \\ rw[]
+  \\ pop_assum mp_tac
+  \\ rw[Once n2l_def]
+  >- ( irule MOD_LESS \\ gs[] )
+  \\ first_x_assum irule
+  \\ gs[DIV_LT_X]
+  \\ Cases_on`b` \\ gs[MULT]
+QED
+
+Definition bool_to_bit_def:
+  bool_to_bit b = if b then 1 else 0
+End
+
+Theorem LENGTH_chunks:
+  ∀n ls. 0 < n ∧ ¬NULL ls ⇒
+    LENGTH (chunks n ls) =
+    LENGTH ls DIV n + (bool_to_bit $ ¬divides n (LENGTH ls))
+Proof
+  recInduct chunks_ind
+  \\ rw[]
+  \\ rw[Once chunks_def, DIV_EQUAL_0, bool_to_bit_def, divides_def]
+  \\ gs[LESS_OR_EQ, ADD1, NULL_EQ, bool_to_bit_def]
+  \\ rw[]
+  \\ gs[divides_def]
+  \\ gs[SUB_DIV]
+  >- (
+    Cases_on`LENGTH ls DIV n = 0` >- gs[DIV_EQUAL_0]
+    \\ simp[] )
+  >- (
+    Cases_on`q` \\ gs[MULT_SUC]
+    \\ qmatch_asmsub_rename_tac`n + n * p`
+    \\ first_x_assum(qspec_then`2 + p`mp_tac)
+    \\ simp[LEFT_ADD_DISTRIB] )
+  >- (
+    first_x_assum(qspec_then`PRE q`mp_tac)
+    \\ Cases_on`q` \\ gs[MULT_SUC] )
+  \\ Cases_on`q` \\ gvs[MULT_SUC]
+  \\ simp[ADD_DIV_RWT]
+QED
+
+Theorem LENGTH_PAD_RIGHT_0_8_word_to_bin_list[simp]:
+  LENGTH (PAD_RIGHT 0 8 (word_to_bin_list (w: word8))) = 8
+Proof
+  rw[word_to_bin_list_def, wordsTheory.w2l_def, PAD_RIGHT, LENGTH_n2l, LOG2_def]
+  \\ Cases_on`w` \\ gs[]
+  \\ rewrite_tac[Once ADD_SYM]
+  \\ irule SUB_ADD
+  \\ `n < 2 ** 8` by simp[]
+  \\ gs[LT_EXP_LOG]
+QED
+
+Theorem l2n_PAD_RIGHT_0[simp]:
+  0 < b ==> l2n b (PAD_RIGHT 0 h ls) = l2n b ls
+Proof
+  Induct_on`ls` \\ rw[l2n_def, PAD_RIGHT, l2n_eq_0, EVERY_GENLIST]
+  \\ gs[PAD_RIGHT, l2n_APPEND]
+  \\ gs[l2n_eq_0, EVERY_GENLIST]
+QED
+
+Theorem BITWISE_COMM:
+  (!m. m <= n ==> op (BIT m x) (BIT m y) = op (BIT m y) (BIT m x))
+  ==> BITWISE n op x y = BITWISE n op y x
+Proof
+  Induct_on`n`
+  \\ rw[BITWISE_def]
+  \\ first_assum(qspec_then`n`mp_tac)
+  \\ impl_tac >- rw[]
+  \\ disch_then SUBST1_TAC
+  \\ simp[]
+  \\ first_x_assum irule
+  \\ rw[]
+  \\ first_x_assum irule
+  \\ simp[]
+QED
+
+Triviality BITWISE_AND_0_lemma:
+  BITWISE w $/\ x 0 = 0
+Proof
+  qid_spec_tac`x`
+  \\ Induct_on`w`
+  \\ rw[BITWISE_def, SBIT_def]
+QED
+
+Theorem BITWISE_AND_0[simp]:
+  BITWISE w $/\ x 0 = 0 /\
+  BITWISE w $/\ 0 x = 0
+Proof
+  qspecl_then[`$/\`,`0`,`x`,`w`]mp_tac(Q.GENL[`op`,`x`,`y`,`n`]BITWISE_COMM)
+  \\ impl_tac >- rw[]
+  \\ disch_then SUBST1_TAC
+  \\ rw[BITWISE_AND_0_lemma]
+QED
+
+Theorem BITWISE_AND_SHIFT_0:
+  !w x y n.
+  x < 2 ** n ==>
+  BITWISE w $/\ x (y * 2 ** n) = 0
+Proof
+  Induct \\ rw[BITWISE_def, SBIT_def]
+  \\ strip_tac
+  \\ Cases_on`w < n`
+  >- ( drule BIT_SHIFT_THM3 \\ simp[]
+       \\ qexists_tac`y` \\ simp[])
+  \\ gs[NOT_LESS]
+  \\ drule TWOEXP_MONO2 \\ strip_tac
+  \\ `x < 2 ** w` by metis_tac[LESS_LESS_EQ_TRANS]
+  \\ drule NOT_BIT_GT_TWOEXP
+  \\ simp[]
+QED
+
+Theorem word_and_lsl_eq_0:
+  w2n w1 < 2 ** n ==> w1 && w2 << n = 0w
+Proof
+  Cases_on`w1` \\ Cases_on`w2`
+  \\ rw[word_and_n2w, word_lsl_n2w]
+  \\ drule BITWISE_AND_SHIFT_0
+  \\ simp[]
+QED
+
+Theorem concat_word_list_bytes_to_64:
+  LENGTH (ls: word8 list) = 8 ⇒
+  concat_word_list ls : word64 =
+  word_from_bin_list (FLAT (MAP (PAD_RIGHT 0 8 o word_to_bin_list) ls))
+Proof
+  simp[LENGTH_EQ_NUM_compute, PULL_EXISTS]
+  \\ qx_genl_tac[`b1`,`b2`,`b3`,`b4`,`b5`,`b6`,`b7`,`b8`]
+  \\ rw[concat_word_list_def]
+  \\ rw[word_from_bin_list_def, l2w_def]
+  \\ rw[l2n_APPEND]
+  \\ rw[word_to_bin_list_def, wordsTheory.w2l_def]
+  \\ simp[l2n_n2l]
+  \\ simp[GSYM word_add_n2w]
+  \\ map_every Cases_on [`b1`,`b2`,`b3`,`b4`,`b5`,`b6`,`b7`,`b8`]
+  \\ gs[]
+  \\ simp[w2w_def]
+  \\ simp[GSYM word_mul_n2w, word_or_n2w]
+  \\ rw(List.tabulate(8, fn i =>
+      WORD_MUL_LSL |> CONV_RULE SWAP_FORALL_CONV
+      |> Q.SPEC`8 * ^(numSyntax.term_of_int i)`
+      |> GSYM |> SIMP_RULE std_ss []))
+  \\ qmatch_goalsub_abbrev_tac `a1 + a2 + a3 + a4 + a5 + a6 + a7 + a8`
+  \\ `∀i m. m < 256 ∧ 8 ≤ i ⇒ ¬BIT i m`
+  by (
+    ntac 3 strip_tac
+    \\ Cases_on`m=0` >- simp[]
+    \\ irule NOT_BIT_GT_LOG2
+    \\ qspecl_then[`m`,`8`]mp_tac LT_TWOEXP
+    \\ simp[] )
+  \\ DEP_REWRITE_TAC[WORD_ADD_OR]
+  \\ rewrite_tac[GSYM WORD_OR_ASSOC]
+  \\ unabbrev_all_tac
+  \\ blastLib.BBLAST_TAC
+  \\ simp[]
+QED
+
 Datatype:
   state_array =
   <| w: num
@@ -1791,10 +1996,6 @@ Theorem index_to_triple_100 =
     EVAL``index_to_triple 4 ^(numLib.term_of_int i)``)
   |> LIST_CONJ
 
-Definition bool_to_bit_def:
-  bool_to_bit b = if b then 1 else 0
-End
-
 Definition bools_to_word_def:
   bools_to_word bs =
   word_from_bin_list (MAP bool_to_bit bs)
@@ -1810,6 +2011,136 @@ Definition bools_to_hex_string_def:
     ) $ chunks 8 bs
 End
 
+Definition pad10s1_136_64w_def:
+  pad10s1_136_64w (zs: word64 list) (m: word8 list) (a: word64 list list) =
+  let lm = LENGTH m in
+  if 136 < lm then let
+    w64s = MAP concat_word_list $ chunks 8 (TAKE 136 m)
+  in pad10s1_136_64w zs (DROP 136 m) ((w64s ++ zs) :: a)
+  else let
+    n = 136 - lm;
+    pad = if n < 1 then [] else
+          if n < 2 then [0x81w] else
+            0x80w::(REPLICATE (n - 2) 0w)++[0x01w];
+    w64s = MAP concat_word_list $ chunks 8 $ m ++ pad
+  in REVERSE $ (w64s ++ zs) :: a
+Termination
+  WF_REL_TAC`measure $ LENGTH o FST o SND`
+  \\ rw[LENGTH_DROP]
+End
+
+(*
+Theorem pad10s1_136_64w_thm:
+  ∀zs bytes acc bools.
+  bools = MAP ((=) 1) $ FLAT $ MAP (PAD_RIGHT 0 8 o word_to_bin_list) bytes ∧
+  zs = REPLICATE (c DIV 64) 0w ∧ c ≠ 0 ∧ divides 64 c
+  ⇒
+  pad10s1_136_64w zs bytes acc =
+  REVERSE acc ++ (
+  MAP (MAP word_from_bin_list o chunks 64) $
+    MAP (λx. MAP bool_to_bit x ++ REPLICATE c 0)
+      (chunks 1088 (bools ++ pad10s1 1088 (LENGTH bools)))
+  )
+Proof
+  recInduct pad10s1_136_64w_ind
+  \\ rw[]
+  \\ simp[Once pad10s1_136_64w_def]
+  \\ IF_CASES_TAC \\ gs[]
+  >- (
+    qmatch_goalsub_abbrev_tac`lhs = _`
+    \\ qspecl_then[`136`,`m`](SUBST1_TAC o SYM)TAKE_DROP
+    \\ qmatch_goalsub_abbrev_tac`MAP _ $ m1 ++ m2`
+    \\ qmatch_goalsub_abbrev_tac`LENGTH bools`
+    \\ qunabbrev_tac`lhs`
+    \\ qmatch_goalsub_abbrev_tac`LENGTH bools2`
+    \\ qmatch_asmsub_abbrev_tac`bools2 = FLAT (MAP fb m2)`
+    \\ `bools = FLAT (MAP fb m1) ++ bools2`
+    by simp[Abbr`bools`]
+    \\ qunabbrev_tac`bools`
+    \\ pop_assum SUBST_ALL_TAC
+    \\ qmatch_goalsub_abbrev_tac`bools1 ++ bools2`
+    \\ `LENGTH m1 = 136` by simp[Abbr`m1`]
+    \\ `LENGTH bools1 = 1088`
+    by (
+      simp[Abbr`bools1`, LENGTH_FLAT, MAP_MAP_o, Abbr`fb`]
+      \\ qmatch_goalsub_abbrev_tac`SUM ls = _`
+      \\ `ls = REPLICATE 136 8`
+      by (
+        simp[Abbr`ls`, LIST_EQ_REWRITE, EL_MAP, EL_REPLICATE]
+        \\ simp[PAD_RIGHT]
+        \\ rpt strip_tac
+        \\ rewrite_tac[Once ADD_SYM]
+        \\ irule SUB_ADD
+        \\ irule LESS_EQ_TRANS
+        \\ qexists_tac`dimindex(:8)`
+        \\ simp[LENGTH_word_to_bin_list_bound] )
+      \\ simp[SUM_REPLICATE] )
+    \\ simp[]
+    \\ rewrite_tac[GSYM APPEND_ASSOC]
+    \\ qmatch_goalsub_abbrev_tac`lhs = _`
+    \\ qmatch_goalsub_abbrev_tac`chunks _ (lm1 ++ lm2)`
+    \\ qspecl_then[`1088`,`lm1`,`lm2`]mp_tac chunks_append_divides
+    \\ impl_tac
+    >- (
+      simp[Abbr`lm1`, NULL_EQ, Abbr`lm2`]
+      \\ conj_tac >- (strip_tac \\ fs[])
+      \\ gs[Abbr`bools2`, pad10s1_def] )
+    \\ disch_then SUBST_ALL_TAC
+    \\ `LENGTH lm1 = 1088` by simp[Abbr`lm1`]
+    \\ first_assum(SUBST1_TAC o SYM)
+    \\ rewrite_tac[chunks_length]
+    \\ simp[Abbr`lhs`]
+    \\ `MAP bool_to_bit lm1 = bools1`
+    by (
+      simp[Abbr`lm1`, MAP_MAP_o, o_DEF]
+      \\ `bools1 = MAP I bools1` by simp[]
+      \\ pop_assum SUBST1_TAC
+      \\ rewrite_tac[MAP_EQ_f, MAP_MAP_o]
+      \\ simp[Abbr`bools1`, MEM_FLAT, PULL_EXISTS, MEM_MAP, Abbr`fb`, PAD_RIGHT,
+              MEM_GENLIST, word_to_bin_list_def]
+      \\ rw[word_to_bin_list_def, bool_to_bit_def]
+      \\ first_assum(mp_then Any mp_tac MEM_w2l_less)
+      \\ simp[] )
+    \\ simp[]
+    \\ qmatch_goalsub_abbrev_tac`bools1 ++ r0`
+    \\ qspecl_then[`64`,`bools1`,`r0`]mp_tac chunks_append_divides
+    \\ impl_tac
+    >- ( simp[NULL_EQ, divides_def, Abbr`r0`] \\ strip_tac \\ gs[] )
+    \\ disch_then SUBST_ALL_TAC
+    \\ simp[Abbr`r0`]
+    \\ qmatch_goalsub_abbrev_tac`l1 ++ l0 = b1 ++ b0`
+    \\ `LENGTH l0 = c DIV 64` by simp[LENGTH_REPLICATE, Abbr`l0`]
+    \\ `LENGTH b0 = c DIV 64` by (
+      simp[Abbr`b0`]
+      \\ DEP_REWRITE_TAC[LENGTH_chunks]
+      \\ simp[LENGTH_REPLICATE, NULL_EQ, bool_to_bit_def] )
+    \\ `LENGTH l1 = 17`
+    by (
+      simp[Abbr`l1`]
+      \\ DEP_REWRITE_TAC[LENGTH_chunks]
+      \\ simp[divides_def, bool_to_bit_def, NULL_EQ]
+      \\ strip_tac \\ gs[] )
+    \\ `LENGTH b1 = 17`
+    by (
+      simp[Abbr`b1`]
+      \\ DEP_REWRITE_TAC[LENGTH_chunks]
+      \\ simp[bool_to_bit_def, divides_def, NULL_EQ]
+      \\ strip_tac \\ gs[] )
+    \\ simp[APPEND_LENGTH_EQ]
+    \\ conj_tac
+    >- (
+      simp[Abbr`l1`, Abbr`b1`, Abbr`bools1`]
+    concat_word_list_bytes_to_64
+*)
+
+Definition Keccak_256_bytes_def:
+  Keccak_256_bytes (bs:word8 list) : word8 list =
+    MAP bools_to_word $ chunks 8 $
+    Keccak_256 $
+    MAP ((=) 1) $ FLAT $
+    MAP (PAD_RIGHT 0 8 o word_to_bin_list) bs
+End
+
 open cv_transLib cv_stdTheory;
 
 val _ = cv_trans index_to_triple_def;

From 616d3cf9bfb13d6096ca7bd0119a9171e624b014 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Fri, 6 Dec 2024 11:26:50 +0000
Subject: [PATCH 02/27] Prove EL_chunks and a bit more progress

---
 examples/Crypto/Keccak/keccakScript.sml | 61 ++++++++++++++++++++++++-
 1 file changed, 60 insertions(+), 1 deletion(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 271ac28ab4..0840a56cb1 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -100,6 +100,31 @@ Proof
   \\ simp[ADD_DIV_RWT]
 QED
 
+Theorem EL_chunks:
+  ∀k ls n.
+  n < LENGTH (chunks k ls) /\ 0 < k /\ ~NULL ls ==>
+  EL n (chunks k ls) = TAKE k (DROP (n * k) ls)
+Proof
+  recInduct chunks_ind \\ rw[NULL_EQ]
+  \\ qpat_x_assum`_ < LENGTH _ `mp_tac
+  \\ rw[Once chunks_def] \\ gs[]
+  >- rw[Once chunks_def]
+  \\ rw[Once chunks_def]
+  \\ qmatch_goalsub_rename_tac`EL m _`
+  \\ Cases_on`m` \\ gs[]
+  \\ pop_assum mp_tac
+  \\ DEP_REWRITE_TAC[LENGTH_chunks]
+  \\ simp[NULL_EQ]
+  \\ strip_tac
+  \\ DEP_REWRITE_TAC[DROP_DROP]
+  \\ simp[MULT_SUC]
+  \\ qmatch_goalsub_rename_tac`n + n * m <= _`
+  \\ `n * m <= LENGTH ls - n` suffices_by simp[]
+  \\ `m <= (LENGTH ls - n) DIV n` suffices_by simp[X_LE_DIV]
+  \\ fs[bool_to_bit_def]
+  \\ pop_assum mp_tac \\ rw[]
+QED
+
 Theorem LENGTH_PAD_RIGHT_0_8_word_to_bin_list[simp]:
   LENGTH (PAD_RIGHT 0 8 (word_to_bin_list (w: word8))) = 8
 Proof
@@ -2130,7 +2155,41 @@ Proof
     \\ conj_tac
     >- (
       simp[Abbr`l1`, Abbr`b1`, Abbr`bools1`]
-    concat_word_list_bytes_to_64
+      \\ reverse conj_tac
+      >- (
+        simp[Abbr`l0`, Abbr`b0`]
+        \\ simp[LIST_EQ_REWRITE, EL_REPLICATE]
+        \\ rpt strip_tac
+        \\ DEP_REWRITE_TAC[EL_MAP]
+        \\ DEP_REWRITE_TAC[LENGTH_chunks]
+        \\ simp[LENGTH_REPLICATE, NULL_EQ]
+        \\ DEP_REWRITE_TAC[EL_chunks]
+        \\ simp[LENGTH_REPLICATE, NULL_EQ]
+        \\ DEP_REWRITE_TAC[LENGTH_chunks]
+        \\ simp[LENGTH_REPLICATE, NULL_EQ]
+        \\ simp[REPLICATE_GENLIST, TAKE_GENLIST]
+        \\ simp[word_from_bin_list_def, l2w_def]
+        \\ qmatch_goalsub_abbrev_tac`A MOD N = 0`
+        \\ `A = 0` suffices_by simp[]
+        \\ qunabbrev_tac`A`
+        \\ simp[l2n_eq_0, EVERY_GENLIST] )
+      \\ simp[LIST_EQ_REWRITE]
+      \\ rpt strip_tac
+      \\ DEP_REWRITE_TAC[EL_MAP]
+      \\ conj_asm1_tac
+      >- (
+        DEP_REWRITE_TAC[LENGTH_chunks]
+        \\ simp[NULL_EQ]
+        \\ (conj_tac \\ strip_tac \\ gs[]))
+      \\ DEP_REWRITE_TAC[EL_chunks]
+      \\ gs[NULL_EQ]
+      \\ conj_tac >- (conj_tac \\ strip_tac \\ gs[])
+      \\ qmatch_goalsub_abbrev_tac`_ ls = _`
+      \\ `LENGTH ls = 8` by simp[Abbr`ls`]
+      \\ drule concat_word_list_bytes_to_64
+      \\ disch_then SUBST_ALL_TAC
+      \\ AP_TERM_TAC
+      \\ simp[Abbr`ls`]
 *)
 
 Definition Keccak_256_bytes_def:

From 267f0f4539a7392b311b5cdffbb440cccb489151 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Fri, 6 Dec 2024 18:48:17 +0000
Subject: [PATCH 03/27] Make progress on pad10s1_136_64w_thm

---
 examples/Crypto/Keccak/keccakScript.sml | 59 ++++++++++++++++++++++++-
 1 file changed, 57 insertions(+), 2 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 0840a56cb1..6deb20ea69 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -2054,7 +2054,36 @@ Termination
   \\ rw[LENGTH_DROP]
 End
 
-(*
+Theorem TAKE_FLAT_bytes[local]:
+  ∀n (ls:word8 list). 8 * (n + 1) ≤ LENGTH ls ==>
+  FLAT (MAP (PAD_RIGHT 0 8 o word_to_bin_list) (TAKE 8 (DROP (8 * n) ls))) =
+  TAKE 64 (DROP (64 * n) (FLAT (MAP (PAD_RIGHT 0 8 o word_to_bin_list) ls)))
+Proof
+  Induct \\ rw[]
+  >- (
+    Cases_on`ls` \\ gs[]
+    \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+    \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+    \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+    \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+    \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+    \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+    \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+    \\ simp[TAKE_APPEND]
+    \\ simp[TAKE_LENGTH_TOO_LONG, LENGTH_PAD_RIGHT_0_8_word_to_bin_list] )
+  \\ gs[LEFT_ADD_DISTRIB, MULT_SUC]
+  \\ Cases_on`ls` \\ gs[]
+  \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+  \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+  \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+  \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+  \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+  \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+  \\ qmatch_asmsub_rename_tac`LENGTH ls` \\ Cases_on`ls` \\ gs[]
+  \\ simp[DROP_APPEND, LENGTH_PAD_RIGHT_0_8_word_to_bin_list,
+          DROP_LENGTH_TOO_LONG]
+QED
+
 Theorem pad10s1_136_64w_thm:
   ∀zs bytes acc bools.
   bools = MAP ((=) 1) $ FLAT $ MAP (PAD_RIGHT 0 8 o word_to_bin_list) bytes ∧
@@ -2190,7 +2219,33 @@ Proof
       \\ disch_then SUBST_ALL_TAC
       \\ AP_TERM_TAC
       \\ simp[Abbr`ls`]
-*)
+      \\ qunabbrev_tac`fb`
+      \\ irule TAKE_FLAT_bytes
+      \\ simp[] )
+    \\ simp[Abbr`lm2`]
+    \\ AP_TERM_TAC
+    \\ AP_TERM_TAC
+    \\ AP_TERM_TAC
+    \\ AP_TERM_TAC
+    \\ simp[pad10s1_def]
+    \\ AP_THM_TAC
+    \\ AP_TERM_TAC
+    \\ qmatch_goalsub_abbrev_tac`A MOD N = B MOD N`
+    \\ `B = A + (N - 1) * N`
+    by (
+      qunabbrev_tac`A`
+      \\ qunabbrev_tac`B`
+      \\ qunabbrev_tac`N`
+      \\ simp[LEFT_ADD_DISTRIB] )
+    \\ qunabbrev_tac`B`
+    \\ pop_assum SUBST_ALL_TAC
+    \\ irule EQ_SYM
+    \\ ONCE_REWRITE_TAC[ADD_COMM]
+    \\ irule MOD_TIMES
+    \\ simp[Abbr`N`] )
+  \\ simp[PULL_EXISTS]
+  \\ cheat
+QED
 
 Definition Keccak_256_bytes_def:
   Keccak_256_bytes (bs:word8 list) : word8 list =

From 1e86dcbb1193814e8a8492f0274627d62edeab93 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 8 Dec 2024 18:05:33 +0000
Subject: [PATCH 04/27] More progress on pad10s1_136_64w thm

---
 examples/Crypto/Keccak/keccakScript.sml | 149 +++++++++++++++++++++++-
 1 file changed, 146 insertions(+), 3 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 6deb20ea69..fce49695bc 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -658,6 +658,19 @@ Proof
   metis_tac[]
 QED
 
+Theorem LENGTH_pad10s1_less:
+  m + 2 ≤ x ==> LENGTH (pad10s1 x m) = x - m
+Proof
+  rw[pad10s1_def, LEFT_ADD_DISTRIB, ADD1]
+  \\ Cases_on`x` \\ gs[]
+  \\ Cases_on`n` \\ gs[ADD1, LEFT_ADD_DISTRIB]
+  \\ qmatch_goalsub_rename_tac`2 * k`
+  \\ `m + (2 * k + (m * k + 2)) = (m + 1) * (k + 2) + (k - m)` by gs[]
+  \\ pop_assum SUBST_ALL_TAC
+  \\ DEP_REWRITE_TAC[MOD_TIMES]
+  \\ simp[]
+QED
+
 Definition Keccak_def:
   Keccak c = sponge (Keccak_p 24) 1600 pad10s1 (1600 - c)
 End
@@ -2042,10 +2055,13 @@ Definition pad10s1_136_64w_def:
   if 136 < lm then let
     w64s = MAP concat_word_list $ chunks 8 (TAKE 136 m)
   in pad10s1_136_64w zs (DROP 136 m) ((w64s ++ zs) :: a)
+  else if lm = 136 then
+    REVERSE $
+      (0x80w::(REPLICATE 134 0w)++(0x01w::zs)) ::
+      ((MAP concat_word_list $ chunks 8 m) ++ zs) :: a
   else let
     n = 136 - lm;
-    pad = if n < 1 then [] else
-          if n < 2 then [0x81w] else
+    pad = if n = 1 then [0x81w] else
             0x80w::(REPLICATE (n - 2) 0w)++[0x01w];
     w64s = MAP concat_word_list $ chunks 8 $ m ++ pad
   in REVERSE $ (w64s ++ zs) :: a
@@ -2243,8 +2259,135 @@ Proof
     \\ ONCE_REWRITE_TAC[ADD_COMM]
     \\ irule MOD_TIMES
     \\ simp[Abbr`N`] )
+  \\ qmatch_goalsub_abbrev_tac`MAP _ $ MAP _ $ chunks _ (l1 ++ l2)`
+  \\ `LENGTH l1 = 8 * LENGTH m`
+  by (
+    simp[Abbr`l1`, LENGTH_FLAT, MAP_MAP_o]
+    \\ qmatch_goalsub_abbrev_tac`SUM ls`
+    \\ `ls = REPLICATE (LENGTH m) 8`
+    by simp[Abbr`ls`, LIST_EQ_REWRITE, EL_MAP, EL_REPLICATE]
+    \\ simp[SUM_REPLICATE] )
+  \\ IF_CASES_TAC \\ gs[]
+  >- (
+    DEP_REWRITE_TAC[chunks_append_divides]
+    \\ simp[NULL_EQ]
+    \\ conj_tac
+    >- (
+      conj_tac >- ( strip_tac \\ gs[] )
+      \\ gs[Abbr`l1`,Abbr`l2`,pad10s1_def] )
+    \\ qpat_assum`LENGTH l1 = _`(SUBST1_TAC o SYM)
+    \\ simp[chunks_length, PULL_EXISTS]
+    \\ `LENGTH l2 = 1088`
+    by ( simp[Abbr`l2`] \\ gs[Abbr`l1`] \\ simp[pad10s1_def] )
+    \\ pop_assum(SUBST1_TAC o SYM)
+    \\ simp[chunks_length]
+    \\ conj_tac
+    >- (
+      DEP_ONCE_REWRITE_TAC[chunks_append_divides]
+      \\ gs[NULL_EQ]
+      \\ conj_tac
+      >- ( conj_tac >- rw[divides_def]
+        \\ strip_tac \\ gs[Abbr`l1`])
+      \\ qmatch_goalsub_abbrev_tac`m1 ++ m2 = m3 ++ m4`
+      \\ `LENGTH m1 = 17`
+      by (
+        simp[Abbr`m1`]
+        \\ DEP_REWRITE_TAC[LENGTH_chunks]
+        \\ simp[divides_def, NULL_EQ, bool_to_bit_def]
+        \\ strip_tac \\ gs[] )
+      \\ `LENGTH m3 = 17`
+      by (
+        simp[Abbr`m3`]
+        \\ DEP_REWRITE_TAC[LENGTH_chunks]
+        \\ gs[bool_to_bit_def, NULL_EQ, divides_def]
+        \\ strip_tac \\ gs[Abbr`l1`]
+        \\ strip_tac \\ gs[] )
+      \\ `LENGTH m2 = c DIV 64` by simp[Abbr`m2`]
+      \\ `LENGTH m4 = c DIV 64` by (
+        simp[Abbr`m4`]
+        \\ DEP_REWRITE_TAC[LENGTH_chunks]
+        \\ simp[bool_to_bit_def, NULL_EQ] )
+      \\ simp[APPEND_LENGTH_EQ]
+      \\ conj_tac
+      >- (
+        gs[Abbr`m1`,Abbr`m3`,LIST_EQ_REWRITE,EL_MAP]
+        \\ rw[]
+        \\ DEP_REWRITE_TAC[EL_chunks]
+        \\ gs[NULL_EQ]
+        \\ conj_tac
+        >- (
+          conj_tac >- (strip_tac \\ gs[])
+          \\ strip_tac \\ gs[Abbr`l1`])
+        \\ gs[Abbr`l1`]
+        \\ simp[MAP_MAP_o, MAP_FLAT]
+        \\ cheat (* TAKE_FLAT_bytes, concat_word_list_bytes_to_64 *) )
+      \\ gs[Abbr`m2`, Abbr`m4`, LIST_EQ_REWRITE, EL_MAP, EL_REPLICATE]
+      \\ rw[]
+      \\ DEP_REWRITE_TAC[EL_chunks]
+      \\ gs[NULL_EQ]
+      \\ simp[word_from_bin_list_def, l2w_def]
+      \\ qmatch_goalsub_abbrev_tac`A MOD N = 0`
+      \\ `A = 0` suffices_by simp[]
+      \\ qunabbrev_tac`A`
+      \\ simp[l2n_eq_0, EVERY_GENLIST, REPLICATE_GENLIST, TAKE_GENLIST])
+    \\ cheat)
   \\ simp[PULL_EXISTS]
-  \\ cheat
+  \\ `LENGTH (l1 ++ l2) = 1088`
+  by (
+    gs[Abbr`l2`, Abbr`l1`]
+    \\ DEP_REWRITE_TAC[LENGTH_pad10s1_less]
+    \\ gs[] )
+  \\ simp[Once chunks_def]
+  \\ qmatch_goalsub_abbrev_tac`chunks 8 ls`
+  \\ `LENGTH ls = 136` by rw[Abbr`ls`]
+  \\ DEP_ONCE_REWRITE_TAC[chunks_append_divides]
+  \\ gs[NULL_EQ]
+  \\ conj_tac
+  >- (
+    conj_tac >- rw[divides_def]
+    \\ strip_tac \\ gs[Abbr`l1`]
+    \\ strip_tac \\ gs[] )
+  \\ qmatch_goalsub_abbrev_tac`m1 ++ m2 = m3 ++ m4`
+  \\ `LENGTH m1 = 17`
+  by (
+    simp[Abbr`m1`]
+    \\ DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ simp[divides_def, NULL_EQ, bool_to_bit_def]
+    \\ strip_tac \\ gs[] )
+  \\ `LENGTH m3 = 17`
+  by (
+    simp[Abbr`m3`]
+    \\ DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ gs[bool_to_bit_def, NULL_EQ, divides_def]
+    \\ strip_tac \\ gs[Abbr`l1`]
+    \\ strip_tac \\ gs[] )
+  \\ `LENGTH m2 = c DIV 64` by simp[Abbr`m2`]
+  \\ `LENGTH m4 = c DIV 64` by (
+    simp[Abbr`m4`]
+    \\ DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ simp[bool_to_bit_def, NULL_EQ] )
+  \\ simp[APPEND_LENGTH_EQ]
+  \\ conj_tac
+  >- (
+    gs[Abbr`m1`,Abbr`m3`,LIST_EQ_REWRITE,EL_MAP]
+    \\ rw[]
+    \\ DEP_REWRITE_TAC[EL_chunks]
+    \\ gs[NULL_EQ]
+    \\ conj_tac
+    >- (
+      conj_tac >- (strip_tac \\ gs[])
+      \\ strip_tac \\ gs[Abbr`l1`]
+      \\ strip_tac \\ gs[] )
+    \\ cheat (* concat_word_list_bytes_to_64, TAKE_FLAT_bytes or similar *) )
+  \\ gs[Abbr`m2`, Abbr`m4`, LIST_EQ_REWRITE, EL_MAP, EL_REPLICATE]
+  \\ rw[]
+  \\ DEP_REWRITE_TAC[EL_chunks]
+  \\ gs[NULL_EQ]
+  \\ simp[word_from_bin_list_def, l2w_def]
+  \\ qmatch_goalsub_abbrev_tac`A MOD N = 0`
+  \\ `A = 0` suffices_by simp[]
+  \\ qunabbrev_tac`A`
+  \\ simp[l2n_eq_0, EVERY_GENLIST, REPLICATE_GENLIST, TAKE_GENLIST]
 QED
 
 Definition Keccak_256_bytes_def:

From 41b366c121f31b9017f9f5470218c79c3142e6f1 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Mon, 9 Dec 2024 08:54:37 +0000
Subject: [PATCH 05/27] Fix part of pad10s1_136_64w and prove some cheats

---
 examples/Crypto/Keccak/keccakScript.sml | 110 +++++++++++++++++++++++-
 1 file changed, 107 insertions(+), 3 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index fce49695bc..8122c6f9c6 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -671,6 +671,18 @@ Proof
   \\ simp[]
 QED
 
+Theorem LENGTH_pad10s1_equal:
+  2 < x ==> LENGTH (pad10s1 x x) = x
+Proof
+  rw[pad10s1_def,ADD1,LEFT_ADD_DISTRIB]
+  \\ qmatch_goalsub_abbrev_tac`a MOD x`
+  \\ `a = (x - 2) + (x * x)` by simp[Abbr`a`]
+  \\ pop_assum SUBST1_TAC
+  \\ DEP_ONCE_REWRITE_TAC[GSYM MOD_PLUS]
+  \\ DEP_REWRITE_TAC[MOD_EQ_0]
+  \\ simp[]
+QED
+
 Definition Keccak_def:
   Keccak c = sponge (Keccak_p 24) 1600 pad10s1 (1600 - c)
 End
@@ -2057,7 +2069,7 @@ Definition pad10s1_136_64w_def:
   in pad10s1_136_64w zs (DROP 136 m) ((w64s ++ zs) :: a)
   else if lm = 136 then
     REVERSE $
-      (0x80w::(REPLICATE 134 0w)++(0x01w::zs)) ::
+      (0x01w::(REPLICATE 15 0w)++(0x8000000000000000w::zs)) ::
       ((MAP concat_word_list $ chunks 8 m) ++ zs) :: a
   else let
     n = 136 - lm;
@@ -2320,7 +2332,28 @@ Proof
           \\ strip_tac \\ gs[Abbr`l1`])
         \\ gs[Abbr`l1`]
         \\ simp[MAP_MAP_o, MAP_FLAT]
-        \\ cheat (* TAKE_FLAT_bytes, concat_word_list_bytes_to_64 *) )
+        \\ qmatch_goalsub_abbrev_tac`MAP (f o g)`
+        \\ `MAP (f o g) m = MAP g m`
+        by (
+          rw[Abbr`f`,Abbr`g`, MAP_EQ_f]
+          \\ qmatch_goalsub_abbrev_tac`MAP _ l`
+          \\ rw[LIST_EQ_REWRITE, EL_MAP]
+          \\ rw[bool_to_bit_def]
+          \\ qmatch_goalsub_abbrev_tac`b =0`
+          \\ `MEM b l` by metis_tac[MEM_EL]
+          \\ pop_assum mp_tac
+          \\ simp[Abbr`l`, PAD_RIGHT, word_to_bin_list_def, MEM_GENLIST]
+          \\ rw[]
+          \\ `b < 2` suffices_by rw[]
+          \\ qspec_then`e`irule(Q.GEN`w`MEM_w2l_less)
+          \\ simp[]
+          \\ metis_tac[])
+        \\ pop_assum SUBST_ALL_TAC
+        \\ qunabbrev_tac`g`
+        \\ DEP_REWRITE_TAC[concat_word_list_bytes_to_64]
+        \\ simp[]
+        \\ DEP_REWRITE_TAC[TAKE_FLAT_bytes]
+        \\ simp[] )
       \\ gs[Abbr`m2`, Abbr`m4`, LIST_EQ_REWRITE, EL_MAP, EL_REPLICATE]
       \\ rw[]
       \\ DEP_REWRITE_TAC[EL_chunks]
@@ -2330,7 +2363,78 @@ Proof
       \\ `A = 0` suffices_by simp[]
       \\ qunabbrev_tac`A`
       \\ simp[l2n_eq_0, EVERY_GENLIST, REPLICATE_GENLIST, TAKE_GENLIST])
-    \\ cheat)
+    \\ gs[Abbr`l1`]
+    \\ simp[Abbr`l2`]
+    \\ DEP_REWRITE_TAC[chunks_append_divides]
+    \\ simp[NULL_EQ, LENGTH_pad10s1_equal]
+    \\ conj_tac >- rw[divides_def, pad10s1_def]
+    \\ once_rewrite_tac[CONS_APPEND]
+    \\ rewrite_tac[APPEND_ASSOC]
+    \\ qmatch_goalsub_abbrev_tac`m1 ++ m2 = m3 ++ m4`
+    \\ `LENGTH m2 = c DIV 64` by simp[Abbr`m2`]
+    \\ `LENGTH m4 = c DIV 64` by (
+      simp[Abbr`m4`]
+      \\ DEP_REWRITE_TAC[LENGTH_chunks]
+      \\ simp[bool_to_bit_def, NULL_EQ] )
+    \\ `LENGTH m1 = 17` by simp[Abbr`m1`]
+    \\ `LENGTH m3 = 17` by (
+      simp[Abbr`m3`]
+      \\ DEP_REWRITE_TAC[LENGTH_chunks]
+      \\ simp[bool_to_bit_def, LENGTH_pad10s1_equal, NULL_EQ, divides_def]
+      \\ simp[pad10s1_def] )
+    \\ simp[APPEND_LENGTH_EQ]
+    \\ reverse conj_tac
+    >- (
+      gs[Abbr`m2`, Abbr`m4`, LIST_EQ_REWRITE, EL_MAP, EL_REPLICATE]
+      \\ rw[]
+      \\ DEP_REWRITE_TAC[EL_chunks]
+      \\ gs[NULL_EQ]
+      \\ simp[word_from_bin_list_def, l2w_def]
+      \\ qmatch_goalsub_abbrev_tac`A MOD N = 0`
+      \\ `A = 0` suffices_by simp[]
+      \\ qunabbrev_tac`A`
+      \\ simp[l2n_eq_0, EVERY_GENLIST, REPLICATE_GENLIST, TAKE_GENLIST] )
+    \\ gs[Abbr`m1`,Abbr`m3`]
+    \\ simp[pad10s1_def, bool_to_bit_def]
+    \\ simp[Once chunks_def]
+    \\ conj_tac
+    >- (
+      simp[TAKE_APPEND]
+      \\ rewrite_tac[REPLICATE_GENLIST, TAKE_GENLIST]
+      \\ simp[] )
+    \\ rewrite_tac[DROP_APPEND, REPLICATE_GENLIST, DROP_GENLIST, LENGTH_GENLIST]
+    \\ qmatch_goalsub_abbrev_tac`chunks _ (GENLIST _ n ++ _)`
+    \\ simp[]
+    \\ simp[Once chunks_def]
+    \\ `~(n + 1 <= 64)` by simp[Abbr`n`]
+    \\ `64 - n = 0` by simp[Abbr`n`]
+    \\ simp[TAKE_APPEND]
+    \\ conj_tac
+    >- (
+      simp[word_from_bin_list_def, l2w_def]
+      \\ qmatch_goalsub_abbrev_tac`A MOD N = 0`
+      \\ `A = 0` suffices_by simp[]
+      \\ qunabbrev_tac`A`
+      \\ simp[l2n_eq_0, EVERY_GENLIST, REPLICATE_GENLIST, TAKE_GENLIST] )
+    \\ simp[DROP_APPEND, DROP_GENLIST]
+    \\ qunabbrev_tac`n`
+    \\ rpt (
+      qmatch_goalsub_abbrev_tac`chunks _ (GENLIST _ n ++ _)`
+      \\ simp[Once chunks_def]
+      \\ `~(n + 1 <= 64)` by simp[Abbr`n`]
+      \\ `64 - n = 0` by simp[Abbr`n`]
+      \\ simp[TAKE_APPEND]
+      \\ conj_tac
+      >- (
+        simp[word_from_bin_list_def, l2w_def]
+        \\ qmatch_goalsub_abbrev_tac`A MOD N = 0`
+        \\ `A = 0` suffices_by simp[]
+        \\ qunabbrev_tac`A`
+        \\ simp[l2n_eq_0, EVERY_GENLIST, REPLICATE_GENLIST, TAKE_GENLIST] )
+      \\ simp[DROP_APPEND, DROP_GENLIST]
+      \\ qunabbrev_tac`n`)
+    \\ gs[]
+    \\ simp[Once chunks_def])
   \\ simp[PULL_EXISTS]
   \\ `LENGTH (l1 ++ l2) = 1088`
   by (

From a86754bb54a335f1b477d6754e5158a4e871430d Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Mon, 9 Dec 2024 10:54:54 +0000
Subject: [PATCH 06/27] Prove remaining cheats in pad10s1_136_64w_thm

---
 examples/Crypto/Keccak/keccakScript.sml | 55 ++++++++++++++++++++++++-
 1 file changed, 53 insertions(+), 2 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 8122c6f9c6..5f2a9bfc31 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -2074,7 +2074,7 @@ Definition pad10s1_136_64w_def:
   else let
     n = 136 - lm;
     pad = if n = 1 then [0x81w] else
-            0x80w::(REPLICATE (n - 2) 0w)++[0x01w];
+            0x01w::(REPLICATE (n - 2) 0w)++[0x80w];
     w64s = MAP concat_word_list $ chunks 8 $ m ++ pad
   in REVERSE $ (w64s ++ zs) :: a
 Termination
@@ -2482,7 +2482,58 @@ Proof
       conj_tac >- (strip_tac \\ gs[])
       \\ strip_tac \\ gs[Abbr`l1`]
       \\ strip_tac \\ gs[] )
-    \\ cheat (* concat_word_list_bytes_to_64, TAKE_FLAT_bytes or similar *) )
+    \\ DEP_REWRITE_TAC[concat_word_list_bytes_to_64]
+    \\ simp[]
+    \\ DEP_REWRITE_TAC[TAKE_FLAT_bytes]
+    \\ simp[]
+    \\ AP_TERM_TAC
+    \\ qunabbrev_tac`ls`
+    \\ AP_TERM_TAC
+    \\ AP_TERM_TAC
+    \\ simp[Abbr`l1`]
+    \\ qmatch_goalsub_abbrev_tac`p1 ++ p2 = p3 ++ p4`
+    \\ `p1 = p3`
+    by (
+      simp[Abbr`p1`,Abbr`p3`,MAP_MAP_o]
+      \\ qmatch_goalsub_abbrev_tac`ls = _`
+      \\ simp[LIST_EQ_REWRITE, EL_MAP, bool_to_bit_def]
+      \\ rw[]
+      \\ qmatch_goalsub_abbrev_tac`b = 0`
+      \\ `MEM b ls` by metis_tac[MEM_EL]
+      \\ pop_assum mp_tac
+      \\ simp[Abbr`ls`, PAD_RIGHT, word_to_bin_list_def,
+              PULL_EXISTS, MEM_GENLIST, MEM_MAP, MEM_FLAT]
+      \\ qx_gen_tac`e` \\ rw[]
+      \\ `b < 2` suffices_by rw[]
+      \\ qspec_then`e`irule(Q.GEN`w`MEM_w2l_less)
+      \\ simp[]
+      \\ metis_tac[])
+    \\ simp[]
+    \\ gs[Abbr`p2`,Abbr`p4`]
+    \\ gs[Abbr`l2`]
+    \\ IF_CASES_TAC
+    >- (
+      `8 * LENGTH m = 1080` by gs[]
+      \\ simp[pad10s1_def, bool_to_bit_def, REPLICATE_GENLIST, PAD_RIGHT] )
+    \\ simp[pad10s1_def, PAD_RIGHT, bool_to_bit_def]
+    \\ simp[REPLICATE_GENLIST]
+    \\ qmatch_goalsub_abbrev_tac`_ = GENLIST _ (n MOD 1088)`
+    \\ gs[]
+    \\ gs[pad10s1_def, ADD1]
+    \\ `n MOD 1088 = 1086 - 8 * LENGTH m` by gs[]
+    \\ pop_assum SUBST1_TAC
+    \\ simp[LIST_EQ_REWRITE, ADD1, LENGTH_FLAT]
+    \\ qmatch_goalsub_abbrev_tac`SUM ls`
+    \\ `ls = REPLICATE (134 - LENGTH m) 8`
+    by simp[Abbr`ls`, LIST_EQ_REWRITE, EL_REPLICATE, EL_MAP]
+    \\ conj_asm1_tac >- simp[SUM_REPLICATE]
+    \\ rw[]
+    \\ qmatch_goalsub_abbrev_tac`EL i ls`
+    \\ `LENGTH ls = 1086 - 8 * LENGTH m`
+    by simp[Abbr`ls`, ADD1, LENGTH_FLAT]
+    \\ `MEM (EL i ls) ls` by metis_tac[MEM_EL]
+    \\ `EVERY (λx. x = 0) ls` suffices_by simp[EVERY_MEM]
+    \\ simp[Abbr`ls`, EVERY_FLAT, EVERY_GENLIST] )
   \\ gs[Abbr`m2`, Abbr`m4`, LIST_EQ_REWRITE, EL_MAP, EL_REPLICATE]
   \\ rw[]
   \\ DEP_REWRITE_TAC[EL_chunks]

From 6b045933e26004761a8bc9895388035bd8522235 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Tue, 10 Dec 2024 12:20:05 +0000
Subject: [PATCH 07/27] Make progress towards w64 version of Keccak_256_bytes

---
 examples/Crypto/Keccak/keccakScript.sml | 191 +++++++++++++++++++++++-
 1 file changed, 190 insertions(+), 1 deletion(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 5f2a9bfc31..480c277128 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -2,7 +2,7 @@ open HolKernel Parse boolLib bossLib dep_rewrite blastLib
      bitLib reduceLib combinLib optionLib sptreeLib wordsLib computeLib;
 open optionTheory pairTheory arithmeticTheory combinTheory listTheory
      rich_listTheory whileTheory bitTheory dividesTheory wordsTheory
-     numposrepTheory logrootTheory sptreeTheory;
+     numposrepTheory numeral_bitTheory logrootTheory sptreeTheory;
 
 (* The SHA-3 Standard: https://doi.org/10.6028/NIST.FIPS.202 *)
 
@@ -10,6 +10,24 @@ val _ = new_theory "keccak";
 
 val _ = numLib.temp_prefer_num();
 
+Theorem DIV2_SBIT:
+  DIV2 (SBIT b n) = if n = 0 then 0 else SBIT b (n - 1)
+Proof
+  qspecl_then[`b`,`n`,`1`]mp_tac SBIT_DIV
+  \\ simp[DIV2_def]
+  \\ Cases_on`1 < n` \\ gs[]
+  \\ Cases_on`n=0` \\ gs[SBIT_def]
+  \\ rw[]
+  \\ `n=1` by gs[]
+  \\ gvs[]
+QED
+
+Theorem ODD_SBIT:
+  ODD (SBIT b n) = (b /\ n = 0)
+Proof
+  rw[SBIT_def, ODD_EXP_IFF]
+QED
+
 Theorem LENGTH_word_to_bin_list_bound:
   LENGTH (word_to_bin_list (w:'a word)) <= (dimindex (:'a))
 Proof
@@ -125,6 +143,34 @@ Proof
   \\ pop_assum mp_tac \\ rw[]
 QED
 
+Theorem chunks_MAP:
+  ∀n ls. chunks n (MAP f ls) = MAP (MAP f) (chunks n ls)
+Proof
+  recInduct chunks_ind \\ rw[]
+  \\ rw[Once chunks_def]
+  >- rw[Once chunks_def]
+  >- rw[Once chunks_def]
+  \\ gs[]
+  \\ simp[GSYM MAP_DROP]
+  \\ simp[Once chunks_def, SimpRHS]
+  \\ simp[MAP_TAKE]
+QED
+
+Theorem chunks_ZIP:
+  ∀n ls l2. LENGTH ls = LENGTH l2 ==>
+  chunks n (ZIP (ls, l2)) = MAP ZIP (ZIP (chunks n ls, chunks n l2))
+Proof
+  recInduct chunks_ind \\ rw[]
+  \\ rw[Once chunks_def]
+  >- ( rw[Once chunks_def] \\ rw[Once chunks_def] )
+  >- rw[Once chunks_def]
+  \\ gs[]
+  \\ simp[GSYM ZIP_DROP]
+  \\ simp[Once chunks_def, SimpRHS]
+  \\ simp[Once chunks_def, SimpR``$,``, SimpRHS]
+  \\ simp[ZIP_TAKE]
+QED
+
 Theorem LENGTH_PAD_RIGHT_0_8_word_to_bin_list[simp]:
   LENGTH (PAD_RIGHT 0 8 (word_to_bin_list (w: word8))) = 8
 Proof
@@ -2545,6 +2591,149 @@ Proof
   \\ simp[l2n_eq_0, EVERY_GENLIST, REPLICATE_GENLIST, TAKE_GENLIST]
 QED
 
+Definition state_bools_64w_def:
+  state_bools_64w bools (w64s:word64 list) =
+  ((LENGTH bools = 1600) ∧
+   (w64s = MAP word_from_bin_list $ chunks 64 $ MAP bool_to_bit bools))
+End
+
+Definition bytes_to_bools_def:
+  bytes_to_bools (bytes: word8 list) =
+    MAP ((=) 1) (FLAT (MAP (PAD_RIGHT 0 8 o word_to_bin_list) bytes))
+End
+
+Theorem pad10s1_136_64w_sponge_init:
+  let
+    N = bytes_to_bools bytes;
+    r = 1600 - 512;
+    P = N ++ pad10s1 r (LENGTH N);
+    c = 1600 - r;
+    Pis = chunks r P;
+    bs = MAP (λPi. Pi ++ REPLICATE c F) Pis
+  in
+    EVERY2 state_bools_64w bs
+    (pad10s1_136_64w (REPLICATE (c DIV 64) 0w) bytes [])
+Proof
+  rw[]
+  \\ qabbrev_tac`c = 512`
+  \\ qmatch_goalsub_abbrev_tac`LENGTH bools`
+  \\ DEP_REWRITE_TAC[pad10s1_136_64w_thm]
+  \\ simp[GSYM bytes_to_bools_def]
+  \\ simp[Abbr`c`, divides_def]
+  \\ simp[LIST_REL_EL_EQN, EL_MAP]
+  \\ simp[state_bools_64w_def, bool_to_bit_def]
+  \\ rw[]
+  \\ DEP_REWRITE_TAC[EL_chunks]
+  \\ conj_asm1_tac
+  >- ( simp[NULL_EQ] \\ simp[Once pad10s1_def] )
+  \\ DEP_REWRITE_TAC[LENGTH_TAKE]
+  \\ simp[DROP_APPEND]
+  \\ pop_assum mp_tac
+  \\ simp[NULL_EQ] \\ strip_tac
+  \\ qpat_x_assum`n < _`mp_tac
+  \\ DEP_REWRITE_TAC[LENGTH_chunks]
+  \\ simp[NULL_EQ]
+  \\ qspecl_then[`1088`,`LENGTH bools`]mp_tac(Q.GENL[`x`,`m`] LENGTH_pad10s1)
+  \\ simp[] \\ strip_tac \\ simp[bool_to_bit_def]
+QED
+
+Theorem word_xor_bits_neq:
+  LENGTH b1 = LENGTH b2 ==>
+  word_from_bin_list b1 ?? word_from_bin_list b2 =
+  word_from_bin_list (MAP (λ(x,y). (x + y) MOD 2) (ZIP (b1, b2)))
+Proof
+  qid_spec_tac`b2`
+  \\ Induct_on`b1`
+  \\ rw[]
+  >- EVAL_TAC
+  \\ Cases_on`b2` \\ gs[]
+  \\ gs[word_from_bin_list_def, l2w_def, l2n_def]
+  \\ gs[GSYM word_add_n2w, GSYM word_mul_n2w]
+  \\ first_x_assum(qspec_then`t`(mp_tac o GSYM))
+  \\ simp[] \\ disch_then kall_tac
+  \\ DEP_REWRITE_TAC[WORD_ADD_XOR]
+  \\ `n2w 2 = n2w (2 ** 1)` by simp[]
+  \\ pop_assum SUBST_ALL_TAC
+  \\ simp[GSYM WORD_MUL_LSL]
+  \\ rewrite_tac[LSL_BITWISE]
+  \\ DEP_REWRITE_TAC[word_and_lsl_eq_0]
+  \\ simp[]
+  \\ conj_tac
+  >- (
+    rw[]
+    \\ Cases_on`2 < dimword(:'a)` \\ gs[MOD_LESS, MOD_MOD_LESS_EQ]
+    \\ Cases_on`dimword(:'a) = 2` \\ gs[MOD_MOD]
+    \\ `dimword(:'a) = 1` by simp[ZERO_LT_dimword]
+    \\ gs[] )
+  \\ rewrite_tac[GSYM WORD_XOR_ASSOC]
+  \\ AP_THM_TAC \\ AP_TERM_TAC
+  \\ AP_THM_TAC \\ AP_TERM_TAC
+  \\ qmatch_goalsub_rename_tac`x + y`
+  \\ `x MOD 2 < 2 ∧ y MOD 2 < 2` by simp[]
+  \\ ntac 2 (pop_assum mp_tac)
+  \\ rewrite_tac[NUMERAL_LESS_THM]
+  \\ Cases_on`ODD (x + y)`
+  >- (
+    `(x + y) MOD 2 = 1` by gs[ODD_MOD2_LEM]
+    \\ gs[ODD_ADD]
+    \\ Cases_on`ODD x` \\ gs[ODD_MOD2_LEM] )
+  \\ gs[GSYM EVEN_ODD]
+  \\ drule (iffLR EVEN_ADD)
+  \\ gs[EVEN_MOD2]
+  \\ Cases_on`x MOD 2 = 0` \\ gs[]
+QED
+
+Theorem xor_state_bools_64w:
+  state_bools_64w b1 w1 /\
+  state_bools_64w b2 w2
+  ==>
+  state_bools_64w (MAP2 (λx y. x ≠ y) b1 b2)
+  (MAP2 word_xor w1 w2)
+Proof
+  rw[state_bools_64w_def]
+  \\ DEP_REWRITE_TAC[MAP2_MAP]
+  \\ simp[chunks_MAP]
+  \\ `LENGTH (chunks 64 b1) = 25 ∧ LENGTH (chunks 64 b2) = 25`
+  by (
+    DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ simp[NULL_EQ, bool_to_bit_def, divides_def]
+    \\ rw[] \\ strip_tac \\ gs[] )
+  \\ simp[chunks_ZIP]
+  \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 1 |> DISCH_ALL]
+  \\ simp[]
+  \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 2 |> DISCH_ALL]
+  \\ simp[MAP_MAP_o]
+  \\ simp[MAP_EQ_f, FORALL_PROD, MEM_ZIP, PULL_EXISTS]
+  \\ rw[]
+  \\ qmatch_goalsub_abbrev_tac`bs1,bs2`
+  \\ `LENGTH bs1 = 64 ∧ LENGTH bs2 = 64`
+  by (
+    simp[Abbr`bs1`,Abbr`bs2`]
+    \\ DEP_REWRITE_TAC[EL_chunks]
+    \\ gs[NULL_EQ, bool_to_bit_def, divides_def]
+    \\ rw[] \\ strip_tac \\ gs[] )
+  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ simp[]
+  \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 1 |> DISCH_ALL]
+  \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 2 |> DISCH_ALL]
+  \\ simp[MAP_MAP_o]
+  \\ AP_TERM_TAC
+  \\ simp[MAP_EQ_f, FORALL_PROD]
+  \\ rw[bool_to_bit_def]
+QED
+
+(*
+
+TODO: define Rnd w64 version
+TODO: define (Keccak_p 24) w64 version
+
+Keccak_256_def
+Keccak_def
+sponge_def
+Keccak_p_def
+Rnd_def
+*)
+
 Definition Keccak_256_bytes_def:
   Keccak_256_bytes (bs:word8 list) : word8 list =
     MAP bools_to_word $ chunks 8 $

From 9b03c4840ebb98a7d3ed82d035c2f0ba23b3584c Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Tue, 10 Dec 2024 20:44:38 +0000
Subject: [PATCH 08/27] Work on theta word64 version

---
 examples/Crypto/Keccak/keccakScript.sml | 170 ++++++++++++++++++++++++
 1 file changed, 170 insertions(+)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 480c277128..6a2fe34eb5 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -36,6 +36,43 @@ Proof
   \\ fs[dimword_def, GSYM LESS_EQ, LOG2_def, LT_EXP_LOG]
 QED
 
+Theorem word_from_bin_list_ror:
+  x < dimindex(:'a) /\ LENGTH ls = dimindex(:'a)
+  ==>
+  word_ror (word_from_bin_list ls : 'a word) x =
+  word_from_bin_list (DROP x ls ++ TAKE x ls)
+Proof
+  rw[word_from_bin_list_def, l2w_def]
+  \\ Cases_on`x = 0` \\ gs[]
+  \\ rw[word_ror_n2w, l2n_APPEND]
+  \\ AP_THM_TAC \\ AP_TERM_TAC
+  \\ qspecl_then[`x`,`ls`](mp_tac o SYM) TAKE_DROP
+  \\ disch_then(SUBST1_TAC o Q.AP_TERM`l2n 2`)
+  \\ rewrite_tac[l2n_APPEND]
+  \\ simp[]
+  \\ qmatch_goalsub_abbrev_tac`BITS _ _ (2 ** x * ld + lt)`
+  \\ qspecl_then[`x - 1`,`0`,`ld`,`lt`]mp_tac BITS_SUM2
+  \\ simp[ADD1]
+  \\ disch_then kall_tac
+  \\ qspecl_then[`x-1`,`lt`]mp_tac BITS_ZEROL
+  \\ simp[ADD1]
+  \\ impl_keep_tac
+  >- (
+    qspecl_then[`TAKE x ls`,`2`]mp_tac l2n_lt
+    \\ simp[] )
+  \\ simp[]
+  \\ disch_then kall_tac
+  \\ simp_tac std_ss [Once ADD_COMM, SimpRHS]
+  \\ qmatch_goalsub_abbrev_tac`BITS h x`
+  \\ qspecl_then[`h`,`x`,`ld`,`lt`]mp_tac BITS_SUM
+  \\ simp[] \\ disch_then kall_tac
+  \\ DEP_REWRITE_TAC[BITS_ZERO4]
+  \\ simp[Abbr`h`]
+  \\ DEP_REWRITE_TAC[BITS_ZEROL]
+  \\ qspecl_then[`DROP x ls`,`2`]mp_tac l2n_lt
+  \\ simp[ADD1]
+QED
+
 Theorem chunks_append_divides:
   ∀n l1 l2.
     0 < n /\ divides n (LENGTH l1) /\ ~NULL l1 /\ ~NULL l2 ==>
@@ -2722,7 +2759,140 @@ Proof
   \\ rw[bool_to_bit_def]
 QED
 
+Definition theta_c_w64_def:
+  theta_c_w64 (s:word64 list) = [
+    EL 0 s ?? EL 5 s ?? EL 10 s ?? EL 15 s ?? EL 20 s;
+    EL 1 s ?? EL 6 s ?? EL 11 s ?? EL 16 s ?? EL 21 s;
+    EL 2 s ?? EL 7 s ?? EL 12 s ?? EL 17 s ?? EL 22 s;
+    EL 3 s ?? EL 8 s ?? EL 13 s ?? EL 18 s ?? EL 23 s;
+    EL 4 s ?? EL 9 s ?? EL 14 s ?? EL 19 s ?? EL 24 s
+  ]
+End
+
+Theorem EL_theta_c_w64:
+  i < 5 ==>
+  EL i (theta_c_w64 s) =
+    EL (i     ) s ??
+    EL (i +  5) s ??
+    EL (i + 10) s ??
+    EL (i + 15) s ??
+    EL (i + 20) s
+Proof
+  rw[theta_c_w64_def, NUMERAL_LESS_THM]
+  \\ rw[]
+QED
+
+Theorem theta_c_w64_thm:
+  state_bools_64w bs ws /\
+  string_to_state_array bs = s /\
+  i < 5
+  ==>
+  EL i (theta_c_w64 ws) =
+  word_from_bin_list $ MAP bool_to_bit $
+  GENLIST (λj. theta_c s.A (i, j)) 64
+Proof
+  strip_tac
+  \\ qmatch_goalsub_abbrev_tac`GENLIST _ n`
+  \\ gvs[state_bools_64w_def]
+  \\ rw[string_to_state_array_def, b2w_def, EL_theta_c_w64]
+  \\ DEP_REWRITE_TAC[EL_MAP]
+  \\ DEP_REWRITE_TAC[LENGTH_chunks]
+  \\ simp[NULL_EQ, bool_to_bit_def]
+  \\ conj_tac >- ( rw[Abbr`n`] \\ strip_tac \\ gs[] )
+  \\ conj_tac >- rw[Abbr`n`, divides_def]
+  \\ DEP_REWRITE_TAC[EL_chunks]
+  \\ DEP_REWRITE_TAC[LENGTH_chunks]
+  \\ qmatch_goalsub_abbrev_tac`GENLIST f`
+  \\ simp[NULL_EQ, bool_to_bit_def]
+  \\ conj_tac >- ( rw[Abbr`n`] \\ strip_tac \\ gs[] )
+  \\ conj_tac >- ( rw[Abbr`n`, divides_def] \\ strip_tac \\ gs[] )
+  \\ simp[GSYM MAP_DROP, GSYM MAP_TAKE]
+  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ conj_tac >- simp[Abbr`n`]
+  \\ AP_TERM_TAC
+  \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 1 |> DISCH_ALL]
+  \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 2 |> DISCH_ALL]
+  \\ rpt (conj_tac >- simp[Abbr`n`])
+  \\ simp[MAP_MAP_o]
+  \\ simp[o_DEF]
+  \\ simp[LIST_EQ_REWRITE]
+  \\ conj_tac >- simp[Abbr`n`]
+  \\ gen_tac
+  \\ DEP_REWRITE_TAC[LENGTH_TAKE]
+  \\ conj_tac >- simp[Abbr`n`]
+  \\ strip_tac
+  \\ simp[EL_MAP]
+  \\ DEP_REWRITE_TAC[EL_MAP]
+  \\ conj_tac >- simp[Abbr`n`]
+  \\ DEP_REWRITE_TAC[EL_ZIP, EL_TAKE, EL_DROP]
+  \\ conj_tac >- simp[Abbr`n`]
+  \\ simp[]
+  \\ simp[Abbr`f`]
+  \\ simp[theta_c_def, restrict_def]
+  \\ rw[bool_to_bit_def]
+QED
+
 (*
+Definition theta_d_w64_def:
+  theta_d_w64 (s:word64 list) =
+  let c = theta_c_w64 s in
+  GENLIST (λx.
+    let
+      idx1 = (x + 4) MOD 5;
+      idx0 = (x + 1) MOD 5;
+      b0 = EL idx0 c;
+    in word_ror b0 63 ?? EL idx1 c
+  ) 5
+End
+
+Theorem theta_d_w64_thm:
+  state_bools_64w bs ws /\
+  string_to_state_array bs = s /\
+  i < 5
+  ==>
+  EL i (theta_d_w64 ws) =
+  word_from_bin_list $ MAP bool_to_bit $
+  GENLIST (λj. theta_d s.w s.A (i,j)) 64
+Proof
+  strip_tac
+  \\ qmatch_goalsub_abbrev_tac`GENLIST _ n`
+  \\ simp[theta_d_def]
+  \\ rewrite_tac[theta_d_w64_def]
+  \\ BasicProvers.LET_ELIM_TAC
+  \\ qmatch_goalsub_abbrev_tac`GENLIST _ m`
+  \\ DEP_REWRITE_TAC[EL_GENLIST]
+  \\ conj_tac >- simp[]
+  \\ BasicProvers.LET_ELIM_TAC
+  \\ qunabbrev_tac`c`
+  \\ qunabbrev_tac`b0`
+  \\ DEP_REWRITE_TAC[theta_c_w64_thm]
+  \\ conj_tac >- gs[Abbr`idx0`,Abbr`idx1`, Abbr`m`]
+  \\ asm_simp_tac std_ss []
+  \\ DEP_REWRITE_TAC[word_from_bin_list_ror]
+  \\ simp[]
+  \\ conj_tac >- rw[Abbr`n`]
+  \\ simp[GSYM MAP_DROP, GSYM MAP_TAKE, DROP_GENLIST, TAKE_GENLIST]
+  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ conj_tac >- simp[Abbr`n`]
+  \\ AP_TERM_TAC
+  \\ rewrite_tac[GSYM MAP_APPEND]
+  \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 1 |> DISCH_ALL]
+  \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 2 |> DISCH_ALL]
+  \\ rpt (conj_tac >- simp[Abbr`n`])
+  \\ simp[MAP_MAP_o, o_DEF]
+  \\ DEP_REWRITE_TAC[ZIP_GENLIST]
+  \\ rpt (conj_tac >- simp[Abbr`n`])
+  \\ simp[MAP_GENLIST, o_DEF]
+  \\ simp[LIST_EQ_REWRITE, EL_APPEND_EQN]
+  \\ rpt strip_tac
+  \\ `s.w = n`
+  by (
+    rw[string_to_state_array_def]
+    \\ gs[state_bools_64w_def, b2w_def] )
+  \\ `MIN 63 n = 63` by simp[Abbr`n`]
+  \\ simp[PRE_SUB1]
+  \\ IF_CASES_TAC
+  >- (
 
 TODO: define Rnd w64 version
 TODO: define (Keccak_p 24) w64 version

From 0c92d4775fcd6f8ecf94bf2c6b03194b6fa1516f Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 11 Dec 2024 00:54:59 +0000
Subject: [PATCH 09/27] More work on theta_w64

---
 examples/Crypto/Keccak/keccakScript.sml | 127 ++++++++++++++++++++----
 1 file changed, 110 insertions(+), 17 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 6a2fe34eb5..50c48f04e7 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -73,6 +73,19 @@ Proof
   \\ simp[ADD1]
 QED
 
+Theorem word_from_bin_list_rol:
+  x < dimindex(:'a) /\ LENGTH ls = dimindex(:'a)
+  ==>
+  word_rol (word_from_bin_list ls : 'a word) x =
+  word_from_bin_list (LASTN x ls ++ BUTLASTN x ls)
+Proof
+  rw[word_rol_def]
+  \\ Cases_on`x=0` \\ gs[]
+  >- simp[LASTN_DROP, BUTLASTN_TAKE, DROP_LENGTH_TOO_LONG, TAKE_LENGTH_TOO_LONG]
+  \\ DEP_REWRITE_TAC[word_from_bin_list_ror]
+  \\ simp[LASTN_DROP, BUTLASTN_TAKE]
+QED
+
 Theorem chunks_append_divides:
   ∀n l1 l2.
     0 < n /\ divides n (LENGTH l1) /\ ~NULL l1 /\ ~NULL l2 ==>
@@ -2832,7 +2845,6 @@ Proof
   \\ rw[bool_to_bit_def]
 QED
 
-(*
 Definition theta_d_w64_def:
   theta_d_w64 (s:word64 list) =
   let c = theta_c_w64 s in
@@ -2841,7 +2853,7 @@ Definition theta_d_w64_def:
       idx1 = (x + 4) MOD 5;
       idx0 = (x + 1) MOD 5;
       b0 = EL idx0 c;
-    in word_ror b0 63 ?? EL idx1 c
+    in word_rol b0 1 ?? EL idx1 c
   ) 5
 End
 
@@ -2868,32 +2880,113 @@ Proof
   \\ DEP_REWRITE_TAC[theta_c_w64_thm]
   \\ conj_tac >- gs[Abbr`idx0`,Abbr`idx1`, Abbr`m`]
   \\ asm_simp_tac std_ss []
-  \\ DEP_REWRITE_TAC[word_from_bin_list_ror]
+  \\ DEP_REWRITE_TAC[word_from_bin_list_rol]
   \\ simp[]
-  \\ conj_tac >- rw[Abbr`n`]
+  \\ conj_asm1_tac >- rw[Abbr`n`]
+  \\ `MIN (n - 1) n = n - 1` by simp[Abbr`n`]
+  \\ simp[LASTN_DROP, BUTLASTN_TAKE]
   \\ simp[GSYM MAP_DROP, GSYM MAP_TAKE, DROP_GENLIST, TAKE_GENLIST]
   \\ DEP_REWRITE_TAC[word_xor_bits_neq]
   \\ conj_tac >- simp[Abbr`n`]
   \\ AP_TERM_TAC
-  \\ rewrite_tac[GSYM MAP_APPEND]
+  \\ rewrite_tac[GSYM MAP_APPEND, GSYM MAP]
   \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 1 |> DISCH_ALL]
   \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 2 |> DISCH_ALL]
   \\ rpt (conj_tac >- simp[Abbr`n`])
   \\ simp[MAP_MAP_o, o_DEF]
-  \\ DEP_REWRITE_TAC[ZIP_GENLIST]
-  \\ rpt (conj_tac >- simp[Abbr`n`])
-  \\ simp[MAP_GENLIST, o_DEF]
-  \\ simp[LIST_EQ_REWRITE, EL_APPEND_EQN]
-  \\ rpt strip_tac
-  \\ `s.w = n`
-  by (
-    rw[string_to_state_array_def]
-    \\ gs[state_bools_64w_def, b2w_def] )
-  \\ `MIN 63 n = 63` by simp[Abbr`n`]
-  \\ simp[PRE_SUB1]
-  \\ IF_CASES_TAC
+  \\ `s.w = n` by ( rw[string_to_state_array_def] \\ gs[state_bools_64w_def, b2w_def] )
+  \\ simp[LIST_EQ_REWRITE, EL_APPEND_EQN, ADD1, EL_MAP, EL_ZIP, PRE_SUB1]
+  \\ Cases \\ simp[bool_to_bit_def] >- rw[]
+  \\ simp[ADD1] \\ rw[]
+QED
+
+Definition theta_w64_def:
+  theta_w64 s =
+  let t = theta_d_w64 s in
+    GENLIST (λi. EL i s ?? EL (i DIV 5) t) 25
+End
+
+Theorem LENGTH_theta_d_w64[simp]:
+  LENGTH (theta_d_w64 s) = 5
+Proof
+  rw[theta_d_w64_def]
+QED
+
+Theorem LENGTH_theta_w64[simp]:
+  LENGTH (theta_w64 s) = 25
+Proof
+  rw[theta_w64_def]
+QED
+
+(*
+Theorem theta_w64_thm:
+  state_bools_64w bs ws /\
+  string_to_state_array bs = s
+  ==>
+  state_bools_64w (state_array_to_string (theta s))
+    $ theta_w64 ws
+Proof
+  simp[state_bools_64w_def]
+  \\ strip_tac
+  \\ conj_tac
+  >- gvs[string_to_state_array_def, b2w_def]
+  \\ simp[theta_def]
+  \\ simp[LIST_EQ_REWRITE]
+  \\ conj_asm1_tac
   >- (
+    DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ simp[NULL_EQ]
+    \\ gvs[string_to_state_array_def, b2w_def, divides_def, bool_to_bit_def]
+    \\ rewrite_tac[state_array_to_string_def]
+    \\ disch_then(mp_tac o Q.AP_TERM`LENGTH`)
+    \\ simp[] )
+  \\ simp[EL_MAP]
+  \\ rewrite_tac[theta_w64_def]
+  \\ gen_tac \\ strip_tac
+  \\ BasicProvers.LET_ELIM_TAC
+  \\ DEP_REWRITE_TAC[EL_GENLIST, EL_MAP]
+  \\ conj_tac
+  >- (
+    DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ gs[NULL_EQ]
+    \\ strip_tac \\ gs[] )
+  \\ qunabbrev_tac`t`
+  \\ DEP_REWRITE_TAC[theta_d_w64_thm]
+  \\ conj_tac
+  >- simp[state_bools_64w_def, DIV_LT_X]
+  \\ DEP_REWRITE_TAC[EL_chunks]
+  \\ conj_tac
+  >- (
+    gs[NULL_EQ]
+    \\ DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ gs[NULL_EQ]
+    \\ rpt strip_tac \\ gs[] )
+  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ conj_tac >- simp[]
+  \\ AP_TERM_TAC
+  \\ rewrite_tac[GSYM MAP_DROP, GSYM MAP_TAKE]
+  \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 1 |> DISCH_ALL]
+  \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 2 |> DISCH_ALL]
+  \\ conj_tac >- rw[]
+  \\ conj_tac >- rw[]
+  \\ rewrite_tac[MAP_MAP_o]
+  \\ qmatch_goalsub_abbrev_tac`ZIP ls`
+  \\ `s.w = 64`
+  by ( rw[] \\ simp[string_to_state_array_def, b2w_def])
+  \\ simp[MAP_MAP_o, LIST_EQ_REWRITE, EL_MAP]
+  \\ conj_asm1_tac
+  >- ( simp[Abbr`ls`, LENGTH_TAKE_EQ])
+  \\ simp[EL_MAP, EL_TAKE, EL_ZIP, Abbr`ls`]
+  \\ qx_gen_tac`i` \\ strip_tac
+  \\ DEP_REWRITE_TAC[EL_DROP]
+  \\ simp[]
+  \\ rewrite_tac[state_array_to_string_compute]
+  \\ DEP_REWRITE_TAC[EL_GENLIST]
+  \\ simp[]
+  \\ simp[restrict_def, DIV_LT_X]
+*)
 
+(*
 TODO: define Rnd w64 version
 TODO: define (Keccak_p 24) w64 version
 

From dbe340edccbffbe45186cf6802aeaa14756ff024 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 11 Dec 2024 09:57:46 +0000
Subject: [PATCH 10/27] Prove theta_w64_thm

---
 examples/Crypto/Keccak/keccakScript.sml | 29 ++++++++++++++++++-------
 1 file changed, 21 insertions(+), 8 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 50c48f04e7..ae2a681df4 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -2900,25 +2900,24 @@ Proof
   \\ simp[ADD1] \\ rw[]
 QED
 
-Definition theta_w64_def:
-  theta_w64 s =
-  let t = theta_d_w64 s in
-    GENLIST (λi. EL i s ?? EL (i DIV 5) t) 25
-End
-
 Theorem LENGTH_theta_d_w64[simp]:
   LENGTH (theta_d_w64 s) = 5
 Proof
   rw[theta_d_w64_def]
 QED
 
+Definition theta_w64_def:
+  theta_w64 s =
+  let t = theta_d_w64 s in
+    GENLIST (λi. EL i s ?? EL (i MOD 5) t) 25
+End
+
 Theorem LENGTH_theta_w64[simp]:
   LENGTH (theta_w64 s) = 25
 Proof
   rw[theta_w64_def]
 QED
 
-(*
 Theorem theta_w64_thm:
   state_bools_64w bs ws /\
   string_to_state_array bs = s
@@ -2984,7 +2983,21 @@ Proof
   \\ DEP_REWRITE_TAC[EL_GENLIST]
   \\ simp[]
   \\ simp[restrict_def, DIV_LT_X]
-*)
+  \\ `i DIV 64 = 0` by simp[DIV_EQ_0]
+  \\ simp[]
+  \\ qmatch_goalsub_abbrev_tac`EL ix bs`
+  \\ qmatch_goalsub_abbrev_tac`s.A t`
+  \\ `EL ix bs = s.A t` suffices_by rw[bool_to_bit_def]
+  \\ rw[string_to_state_array_def, b2w_def, Abbr`t`, restrict_def, DIV_LT_X]
+  \\ rw[Abbr`ix`]
+  \\ AP_THM_TAC
+  \\ AP_TERM_TAC
+  \\ simp[]
+  \\ qspec_then`5`mp_tac DIVISION
+  \\ impl_tac >- rw[]
+  \\ disch_then(qspec_then`x`mp_tac)
+  \\ simp[]
+QED
 
 (*
 TODO: define Rnd w64 version

From 3c58be89bc5dc3ae33264382499011223832fe2f Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 11 Dec 2024 10:05:12 +0000
Subject: [PATCH 11/27] Use w64 suffix consistently

---
 examples/Crypto/Keccak/keccakScript.sml | 60 ++++++++++++++-----------
 1 file changed, 33 insertions(+), 27 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index ae2a681df4..fdb87b061f 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -2157,12 +2157,12 @@ Definition bools_to_hex_string_def:
     ) $ chunks 8 bs
 End
 
-Definition pad10s1_136_64w_def:
-  pad10s1_136_64w (zs: word64 list) (m: word8 list) (a: word64 list list) =
+Definition pad10s1_136_w64_def:
+  pad10s1_136_w64 (zs: word64 list) (m: word8 list) (a: word64 list list) =
   let lm = LENGTH m in
   if 136 < lm then let
     w64s = MAP concat_word_list $ chunks 8 (TAKE 136 m)
-  in pad10s1_136_64w zs (DROP 136 m) ((w64s ++ zs) :: a)
+  in pad10s1_136_w64 zs (DROP 136 m) ((w64s ++ zs) :: a)
   else if lm = 136 then
     REVERSE $
       (0x01w::(REPLICATE 15 0w)++(0x8000000000000000w::zs)) ::
@@ -2208,21 +2208,21 @@ Proof
           DROP_LENGTH_TOO_LONG]
 QED
 
-Theorem pad10s1_136_64w_thm:
+Theorem pad10s1_136_w64_thm:
   ∀zs bytes acc bools.
   bools = MAP ((=) 1) $ FLAT $ MAP (PAD_RIGHT 0 8 o word_to_bin_list) bytes ∧
   zs = REPLICATE (c DIV 64) 0w ∧ c ≠ 0 ∧ divides 64 c
   ⇒
-  pad10s1_136_64w zs bytes acc =
+  pad10s1_136_w64 zs bytes acc =
   REVERSE acc ++ (
   MAP (MAP word_from_bin_list o chunks 64) $
     MAP (λx. MAP bool_to_bit x ++ REPLICATE c 0)
       (chunks 1088 (bools ++ pad10s1 1088 (LENGTH bools)))
   )
 Proof
-  recInduct pad10s1_136_64w_ind
+  recInduct pad10s1_136_w64_ind
   \\ rw[]
-  \\ simp[Once pad10s1_136_64w_def]
+  \\ simp[Once pad10s1_136_w64_def]
   \\ IF_CASES_TAC \\ gs[]
   >- (
     qmatch_goalsub_abbrev_tac`lhs = _`
@@ -2641,8 +2641,8 @@ Proof
   \\ simp[l2n_eq_0, EVERY_GENLIST, REPLICATE_GENLIST, TAKE_GENLIST]
 QED
 
-Definition state_bools_64w_def:
-  state_bools_64w bools (w64s:word64 list) =
+Definition state_bools_w64_def:
+  state_bools_w64 bools (w64s:word64 list) =
   ((LENGTH bools = 1600) ∧
    (w64s = MAP word_from_bin_list $ chunks 64 $ MAP bool_to_bit bools))
 End
@@ -2652,7 +2652,7 @@ Definition bytes_to_bools_def:
     MAP ((=) 1) (FLAT (MAP (PAD_RIGHT 0 8 o word_to_bin_list) bytes))
 End
 
-Theorem pad10s1_136_64w_sponge_init:
+Theorem pad10s1_136_w64_sponge_init:
   let
     N = bytes_to_bools bytes;
     r = 1600 - 512;
@@ -2661,17 +2661,17 @@ Theorem pad10s1_136_64w_sponge_init:
     Pis = chunks r P;
     bs = MAP (λPi. Pi ++ REPLICATE c F) Pis
   in
-    EVERY2 state_bools_64w bs
-    (pad10s1_136_64w (REPLICATE (c DIV 64) 0w) bytes [])
+    EVERY2 state_bools_w64 bs
+    (pad10s1_136_w64 (REPLICATE (c DIV 64) 0w) bytes [])
 Proof
   rw[]
   \\ qabbrev_tac`c = 512`
   \\ qmatch_goalsub_abbrev_tac`LENGTH bools`
-  \\ DEP_REWRITE_TAC[pad10s1_136_64w_thm]
+  \\ DEP_REWRITE_TAC[pad10s1_136_w64_thm]
   \\ simp[GSYM bytes_to_bools_def]
   \\ simp[Abbr`c`, divides_def]
   \\ simp[LIST_REL_EL_EQN, EL_MAP]
-  \\ simp[state_bools_64w_def, bool_to_bit_def]
+  \\ simp[state_bools_w64_def, bool_to_bit_def]
   \\ rw[]
   \\ DEP_REWRITE_TAC[EL_chunks]
   \\ conj_asm1_tac
@@ -2733,14 +2733,14 @@ Proof
   \\ Cases_on`x MOD 2 = 0` \\ gs[]
 QED
 
-Theorem xor_state_bools_64w:
-  state_bools_64w b1 w1 /\
-  state_bools_64w b2 w2
+Theorem xor_state_bools_w64:
+  state_bools_w64 b1 w1 /\
+  state_bools_w64 b2 w2
   ==>
-  state_bools_64w (MAP2 (λx y. x ≠ y) b1 b2)
+  state_bools_w64 (MAP2 (λx y. x ≠ y) b1 b2)
   (MAP2 word_xor w1 w2)
 Proof
-  rw[state_bools_64w_def]
+  rw[state_bools_w64_def]
   \\ DEP_REWRITE_TAC[MAP2_MAP]
   \\ simp[chunks_MAP]
   \\ `LENGTH (chunks 64 b1) = 25 ∧ LENGTH (chunks 64 b2) = 25`
@@ -2796,7 +2796,7 @@ Proof
 QED
 
 Theorem theta_c_w64_thm:
-  state_bools_64w bs ws /\
+  state_bools_w64 bs ws /\
   string_to_state_array bs = s /\
   i < 5
   ==>
@@ -2806,7 +2806,7 @@ Theorem theta_c_w64_thm:
 Proof
   strip_tac
   \\ qmatch_goalsub_abbrev_tac`GENLIST _ n`
-  \\ gvs[state_bools_64w_def]
+  \\ gvs[state_bools_w64_def]
   \\ rw[string_to_state_array_def, b2w_def, EL_theta_c_w64]
   \\ DEP_REWRITE_TAC[EL_MAP]
   \\ DEP_REWRITE_TAC[LENGTH_chunks]
@@ -2858,7 +2858,7 @@ Definition theta_d_w64_def:
 End
 
 Theorem theta_d_w64_thm:
-  state_bools_64w bs ws /\
+  state_bools_w64 bs ws /\
   string_to_state_array bs = s /\
   i < 5
   ==>
@@ -2894,7 +2894,7 @@ Proof
   \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 2 |> DISCH_ALL]
   \\ rpt (conj_tac >- simp[Abbr`n`])
   \\ simp[MAP_MAP_o, o_DEF]
-  \\ `s.w = n` by ( rw[string_to_state_array_def] \\ gs[state_bools_64w_def, b2w_def] )
+  \\ `s.w = n` by ( rw[string_to_state_array_def] \\ gs[state_bools_w64_def, b2w_def] )
   \\ simp[LIST_EQ_REWRITE, EL_APPEND_EQN, ADD1, EL_MAP, EL_ZIP, PRE_SUB1]
   \\ Cases \\ simp[bool_to_bit_def] >- rw[]
   \\ simp[ADD1] \\ rw[]
@@ -2919,13 +2919,13 @@ Proof
 QED
 
 Theorem theta_w64_thm:
-  state_bools_64w bs ws /\
+  state_bools_w64 bs ws /\
   string_to_state_array bs = s
   ==>
-  state_bools_64w (state_array_to_string (theta s))
+  state_bools_w64 (state_array_to_string (theta s))
     $ theta_w64 ws
 Proof
-  simp[state_bools_64w_def]
+  simp[state_bools_w64_def]
   \\ strip_tac
   \\ conj_tac
   >- gvs[string_to_state_array_def, b2w_def]
@@ -2952,7 +2952,7 @@ Proof
   \\ qunabbrev_tac`t`
   \\ DEP_REWRITE_TAC[theta_d_w64_thm]
   \\ conj_tac
-  >- simp[state_bools_64w_def, DIV_LT_X]
+  >- simp[state_bools_w64_def, DIV_LT_X]
   \\ DEP_REWRITE_TAC[EL_chunks]
   \\ conj_tac
   >- (
@@ -3003,11 +3003,17 @@ QED
 TODO: define Rnd w64 version
 TODO: define (Keccak_p 24) w64 version
 
+Definition rho_w64_def:
+End
+
 Keccak_256_def
 Keccak_def
 sponge_def
 Keccak_p_def
 Rnd_def
+rho_def
+rho_spt_def
+rho_xy_def
 *)
 
 Definition Keccak_256_bytes_def:

From 2bfdd3e3189eb12aa10d1fbd28576320161afcdb Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 11 Dec 2024 16:27:08 +0000
Subject: [PATCH 12/27] Prove rho_w64_thm

---
 examples/Crypto/Keccak/keccakScript.sml | 236 +++++++++++++++++++++++-
 1 file changed, 230 insertions(+), 6 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index fdb87b061f..7d8f0152f5 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -2999,21 +2999,245 @@ Proof
   \\ simp[]
 QED
 
-(*
-TODO: define Rnd w64 version
-TODO: define (Keccak_p 24) w64 version
+Theorem rho_xy_invert:
+  t <= 23 ==>
+  (rho_xy t = (1,0) ==> t = 00) ∧
+  (rho_xy t = (2,0) ==> t = 18) ∧
+  (rho_xy t = (3,0) ==> t = 06) ∧
+  (rho_xy t = (4,0) ==> t = 12) ∧
+  (rho_xy t = (0,1) ==> t = 07) ∧
+  (rho_xy t = (1,1) ==> t = 23) ∧
+  (rho_xy t = (2,1) ==> t = 02) ∧
+  (rho_xy t = (3,1) ==> t = 09) ∧
+  (rho_xy t = (4,1) ==> t = 22) ∧
+  (rho_xy t = (0,2) ==> t = 01) ∧
+  (rho_xy t = (1,2) ==> t = 03) ∧
+  (rho_xy t = (2,2) ==> t = 17) ∧
+  (rho_xy t = (3,2) ==> t = 16) ∧
+  (rho_xy t = (4,2) ==> t = 20) ∧
+  (rho_xy t = (0,3) ==> t = 13) ∧
+  (rho_xy t = (1,3) ==> t = 08) ∧
+  (rho_xy t = (2,3) ==> t = 04) ∧
+  (rho_xy t = (3,3) ==> t = 05) ∧
+  (rho_xy t = (4,3) ==> t = 15) ∧
+  (rho_xy t = (0,4) ==> t = 19) ∧
+  (rho_xy t = (1,4) ==> t = 10) ∧
+  (rho_xy t = (2,4) ==> t = 21) ∧
+  (rho_xy t = (3,4) ==> t = 14) ∧
+  (rho_xy t = (4,4) ==> t = 11)
+Proof
+  simp[LESS_OR_EQ]
+  \\ CONV_TAC(LAND_CONV(SIMP_CONV std_ss [NUMERAL_LESS_THM]))
+  \\ strip_tac
+  \\ BasicProvers.VAR_EQ_TAC
+  \\ EVAL_TAC
+QED
+
+Definition rho_w64_shifts_def:
+  rho_w64_shifts =
+    MAP (λt. (19200 - (((t + 1) * (t + 2)) DIV 2)) MOD 64)
+    [00 ;18 ;06 ;12 ;07 ;23 ;02 ;09 ;22 ;01 ;03 ;17 ;16
+    ;20 ;13 ;08 ;04 ;05 ;15 ;19 ;10 ;21 ;14 ;11]
+End
 
 Definition rho_w64_def:
+  rho_w64 (s: word64 list) =
+  HD s ::
+  GENLIST (λi.
+    word_ror (EL (SUC i) s) (EL i rho_w64_shifts)
+  ) 24
 End
 
+Theorem rho_w64_thm:
+  state_bools_w64 bs ws ∧
+  string_to_state_array bs = s ⇒
+  state_bools_w64 (state_array_to_string (rho s)) (rho_w64 ws)
+Proof
+  simp[state_bools_w64_def]
+  \\ strip_tac
+  \\ conj_asm1_tac
+  >- rw[string_to_state_array_def, b2w_def]
+  \\ rewrite_tac[rho_def, rho_w64_def]
+  \\ qmatch_goalsub_abbrev_tac`GENLIST _ n`
+  \\ rewrite_tac[state_array_to_string_compute]
+  \\ qmatch_goalsub_abbrev_tac`5 * 5 * sw`
+  \\ `sw = s.w` by rw[Abbr`sw`]
+  \\ qabbrev_tac`m = 5 * 5 * sw`
+  \\ simp[restrict_def]
+  \\ qmatch_goalsub_abbrev_tac`GENLIST f m`
+  \\ simp[LIST_EQ_REWRITE]
+  \\ DEP_REWRITE_TAC[LENGTH_chunks]
+  \\ rewrite_tac[NULL_LENGTH, LENGTH_MAP, LENGTH_GENLIST]
+  \\ conj_asm1_tac >- rw[Abbr`m`]
+  \\ conj_asm1_tac >- rw[Abbr`m`, divides_def, bool_to_bit_def, Abbr`n`]
+  \\ pop_assum(assume_tac o SYM)
+  \\ Cases
+  >- (
+    simp[]
+    \\ rewrite_tac[GSYM EL]
+    \\ DEP_REWRITE_TAC[EL_MAP]
+    \\ DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ rewrite_tac[NULL_LENGTH, LENGTH_MAP, LENGTH_GENLIST]
+    \\ simp[] \\ conj_tac >- (strip_tac \\ gs[])
+    \\ AP_TERM_TAC
+    \\ rewrite_tac[GSYM EL]
+    \\ DEP_REWRITE_TAC[EL_chunks]
+    \\ DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ rewrite_tac[NULL_LENGTH, LENGTH_MAP, LENGTH_GENLIST]
+    \\ simp[] \\ conj_tac >- (strip_tac \\ gs[])
+    \\ conj_tac >- (strip_tac \\ gs[])
+    \\ simp[LIST_EQ_REWRITE, LENGTH_TAKE_EQ]
+    \\ conj_tac >- rw[Abbr`m`]
+    \\ rw[]
+    \\ DEP_REWRITE_TAC[EL_TAKE, EL_MAP, EL_GENLIST]
+    \\ conj_tac >- rw[Abbr`m`]
+    \\ simp[Abbr`f`, DIV_EQ_0, DIV_LT_X]
+    \\ rw[string_to_state_array_def, restrict_def, b2w_def] )
+  \\ simp[]
+  \\ strip_tac
+  \\ DEP_REWRITE_TAC[EL_MAP]
+  \\ DEP_REWRITE_TAC[LENGTH_chunks]
+  \\ rewrite_tac[NULL_LENGTH, LENGTH_MAP, LENGTH_GENLIST]
+  \\ simp[] \\ conj_tac >- (strip_tac \\ gs[])
+  \\ conj_tac >- ( rw[bool_to_bit_def, divides_def] \\ gvs[Abbr`n`] )
+  \\ DEP_REWRITE_TAC[EL_chunks]
+  \\ DEP_REWRITE_TAC[LENGTH_chunks]
+  \\ rewrite_tac[NULL_LENGTH, LENGTH_MAP, LENGTH_GENLIST]
+  \\ simp[] \\ conj_tac >- (strip_tac \\ gs[])
+  \\ conj_tac >- ( rw[bool_to_bit_def, divides_def] \\ gvs[Abbr`n`] )
+  \\ simp[GSYM MAP_DROP, GSYM TAKE_DROP, DROP_GENLIST]
+  \\ DEP_REWRITE_TAC[word_from_bin_list_ror]
+  \\ simp[LENGTH_TAKE_EQ]
+  \\ qmatch_asmsub_rename_tac`p < n`
+  \\ `p < 24` by gs[Abbr`n`]
+  \\ simp[]
+  \\ conj_asm1_tac
+  >- (
+    rewrite_tac[rho_w64_shifts_def]
+    \\ DEP_REWRITE_TAC[EL_MAP]
+    \\ simp[] )
+  \\ AP_TERM_TAC
+  \\ simp[LIST_EQ_REWRITE]
+  \\ DEP_REWRITE_TAC[LENGTH_TAKE_EQ, LENGTH_BUTLASTN, LENGTH_LASTN]
+  \\ simp[]
+  \\ conj_tac >- rw[Abbr`m`]
+  \\ rpt strip_tac
+  \\ DEP_REWRITE_TAC[EL_APPEND_EQN]
+  \\ DEP_REWRITE_TAC[LENGTH_TAKE_EQ, LENGTH_BUTLASTN, LENGTH_LASTN]
+  \\ simp[]
+  \\ DEP_REWRITE_TAC[EL_TAKE, EL_MAP, EL_GENLIST]
+  \\ simp[]
+  \\ conj_tac >- (
+    rw[Abbr`m`]
+    \\ qpat_x_assum`p < _`mp_tac
+    \\ simp_tac std_ss [NUMERAL_LESS_THM]
+    \\ strip_tac \\ BasicProvers.VAR_EQ_TAC \\ EVAL_TAC )
+  \\ DEP_REWRITE_TAC[LASTN_DROP, BUTLASTN_TAKE]
+  \\ simp[]
+  \\ `x DIV 64 = 0` by simp[DIV_EQ_0]
+  \\ qunabbrev_tac`f`
+  \\ simp[DIV_LT_X]
+  \\ qmatch_goalsub_abbrev_tac`t + 2`
+  \\ IF_CASES_TAC
+  >- (
+    DEP_REWRITE_TAC[EL_DROP, EL_TAKE, EL_MAP]
+    \\ simp[]
+    \\ AP_TERM_TAC
+    \\ IF_CASES_TAC
+    >- (
+      pop_assum mp_tac
+      \\ qpat_x_assum`p < 24`mp_tac
+      \\ CONV_TAC(LAND_CONV(SIMP_CONV std_ss [NUMERAL_LESS_THM]))
+      \\ strip_tac \\ simp[]
+      \\ simp[Abbr`n`] )
+    \\ qunabbrev_tac`t`
+    \\ numLib.LEAST_ELIM_TAC
+    \\ first_assum(mp_then Any mp_tac rho_xy_exists)
+    \\ impl_tac >- simp[DIV_LT_X]
+    \\ strip_tac
+    \\ conj_tac >- (qexists_tac`t` \\ simp[])
+    \\ qx_gen_tac`t2`
+    \\ strip_tac
+    \\ `¬(t < t2)` by metis_tac[]
+    \\ `t2 <= 23` by gs[]
+    \\ rw[string_to_state_array_def, restrict_def, DIV_LT_X, b2w_def]
+    \\ AP_THM_TAC
+    \\ AP_TERM_TAC
+    \\ qpat_x_assum`_ = _.w`kall_tac
+    \\ qpat_x_assum`x < _ -_`mp_tac
+    \\ rewrite_tac[rho_w64_shifts_def]
+    \\ qunabbrev_tac`n`
+    \\ drule rho_xy_invert \\ strip_tac
+    \\ qpat_x_assum`x < _`mp_tac
+    \\ qpat_x_assum`p < _`mp_tac
+    \\ CONV_TAC(LAND_CONV(SIMP_CONV std_ss [NUMERAL_LESS_THM]))
+    \\ strip_tac
+    \\ BasicProvers.VAR_EQ_TAC
+    \\ qpat_x_assum`rho_xy _ = _`mp_tac
+    \\ simp_tac std_ss [] \\ strip_tac
+    \\ first_x_assum drule
+    \\ strip_tac
+    \\ BasicProvers.VAR_EQ_TAC
+    \\ DEP_REWRITE_TAC[EL_MAP]
+    \\ simp_tac (srw_ss()) []
+    \\ rw[])
+  \\ DEP_REWRITE_TAC[EL_DROP]
+  \\ simp[]
+  \\ AP_TERM_TAC
+  \\ IF_CASES_TAC
+  >- (
+    pop_assum mp_tac
+    \\ qpat_x_assum`p < 24`mp_tac
+    \\ CONV_TAC(LAND_CONV(SIMP_CONV std_ss [NUMERAL_LESS_THM]))
+    \\ strip_tac \\ simp[]
+    \\ simp[Abbr`n`] )
+  \\ qunabbrev_tac`t`
+  \\ numLib.LEAST_ELIM_TAC
+  \\ first_assum(mp_then Any mp_tac rho_xy_exists)
+  \\ impl_tac >- simp[DIV_LT_X]
+  \\ strip_tac
+  \\ conj_tac >- (qexists_tac`t` \\ simp[])
+  \\ qx_gen_tac`t2`
+  \\ strip_tac
+  \\ `¬(t < t2)` by metis_tac[]
+  \\ `t2 <= 23` by gs[]
+  \\ rw[string_to_state_array_def, restrict_def, DIV_LT_X, b2w_def]
+  \\ AP_THM_TAC
+  \\ AP_TERM_TAC
+  \\ qpat_x_assum`_ = _.w`kall_tac
+  \\ qpat_x_assum`~(x < _ -_)`mp_tac
+  \\ rewrite_tac[rho_w64_shifts_def]
+  \\ qunabbrev_tac`n`
+  \\ drule rho_xy_invert \\ strip_tac
+  \\ qpat_x_assum`x < _`mp_tac
+  \\ qpat_x_assum`p < _`mp_tac
+  \\ CONV_TAC(LAND_CONV(SIMP_CONV std_ss [NUMERAL_LESS_THM]))
+  \\ strip_tac
+  \\ BasicProvers.VAR_EQ_TAC
+  \\ qpat_x_assum`rho_xy _ = _`mp_tac
+  \\ simp_tac std_ss [] \\ strip_tac
+  \\ first_x_assum drule
+  \\ strip_tac
+  \\ BasicProvers.VAR_EQ_TAC
+  \\ DEP_REWRITE_TAC[EL_MAP]
+  \\ simp_tac (srw_ss()) []
+  \\ CONV_TAC(LAND_CONV(SIMP_CONV std_ss [NUMERAL_LESS_THM]))
+  \\ strip_tac \\ BasicProvers.VAR_EQ_TAC
+  \\ EVAL_TAC
+QED
+
+(*
+TODO: define Rnd w64 version
+TODO: define (Keccak_p 24) w64 version
+
 Keccak_256_def
 Keccak_def
 sponge_def
 Keccak_p_def
 Rnd_def
-rho_def
-rho_spt_def
-rho_xy_def
+pi_def
+chi_def
+iota_compute
 *)
 
 Definition Keccak_256_bytes_def:

From 14b00962b21cbc4d93b879ee3d029e2905142b42 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 11 Dec 2024 16:39:46 +0000
Subject: [PATCH 13/27] Add MAP2 version of rho_w64

---
 examples/Crypto/Keccak/keccakScript.sml | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 7d8f0152f5..7daeb1a95b 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -3040,6 +3040,12 @@ Definition rho_w64_shifts_def:
     ;20 ;13 ;08 ;04 ;05 ;15 ;19 ;10 ;21 ;14 ;11]
 End
 
+Theorem LENGTH_rho_w64_shifts[simp]:
+  LENGTH rho_w64_shifts = 24
+Proof
+  rw[rho_w64_shifts_def]
+QED
+
 Definition rho_w64_def:
   rho_w64 (s: word64 list) =
   HD s ::
@@ -3226,6 +3232,25 @@ Proof
   \\ EVAL_TAC
 QED
 
+Theorem rho_w64_MAP2:
+  LENGTH s = 25 ==>
+  rho_w64 s =
+  case s of h::t =>
+    h :: MAP2 (λx y. word_ror x y) t rho_w64_shifts
+  | _ => []
+Proof
+  strip_tac
+  \\ CASE_TAC >- fs[]
+  \\ rewrite_tac[LIST_EQ_REWRITE]
+  \\ conj_tac >- gs[rho_w64_def, LENGTH_TL, ADD1, MIN_DEF]
+  \\ Cases >- rw[rho_w64_def]
+  \\ strip_tac
+  \\ rewrite_tac[rho_w64_def]
+  \\ DEP_REWRITE_TAC[EL_CONS, EL_GENLIST, EL_MAP2]
+  \\ conj_tac >- fs[rho_w64_def, LENGTH_TL]
+  \\ simp[]
+QED
+
 (*
 TODO: define Rnd w64 version
 TODO: define (Keccak_p 24) w64 version

From 32658d27d423a495b49b29fa5d134bed803a5848 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Thu, 12 Dec 2024 07:40:42 +0000
Subject: [PATCH 14/27] Prove pi_w64_thm

---
 examples/Crypto/Keccak/keccakScript.sml | 90 ++++++++++++++++++++++++-
 1 file changed, 89 insertions(+), 1 deletion(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 7daeb1a95b..1801be45d9 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -10,6 +10,15 @@ val _ = new_theory "keccak";
 
 val _ = numLib.temp_prefer_num();
 
+Theorem GENLIST_EQ_NIL[simp]:
+  GENLIST f n = [] <=> n = 0
+Proof
+  rw[EQ_IMP_THM]
+  \\ pop_assum(mp_tac o Q.AP_TERM`LENGTH`)
+  \\ rewrite_tac[LENGTH_GENLIST]
+  \\ rw[]
+QED
+
 Theorem DIV2_SBIT:
   DIV2 (SBIT b n) = if n = 0 then 0 else SBIT b (n - 1)
 Proof
@@ -3251,6 +3260,82 @@ Proof
   \\ simp[]
 QED
 
+Definition pi_w64_indices_def:
+  pi_w64_indices =
+  GENLIST (λi. let
+    x = i MOD 5;
+    y = i DIV 5;
+    x' = (x + 3 * y) MOD 5 in
+      x' + 5 * x) 25
+End
+
+Theorem pi_w64_indices_eq = EVAL ``pi_w64_indices``;
+
+Theorem pi_w64_indices_bound:
+  EVERY ($> 25) pi_w64_indices
+Proof
+  rw[pi_w64_indices_eq]
+QED
+
+Definition pi_w64_def:
+  pi_w64 (s: word64 list) =
+  MAP (λi. EL i s) pi_w64_indices
+End
+
+Theorem pi_w64_thm:
+  state_bools_w64 bs ws ∧
+  string_to_state_array bs = s ⇒
+  state_bools_w64 (state_array_to_string (pi s)) (pi_w64 ws)
+Proof
+  strip_tac
+  \\ gs[state_bools_w64_def]
+  \\ conj_asm1_tac >- rw[string_to_state_array_def, b2w_def]
+  \\ simp[pi_def, pi_w64_def]
+  \\ rewrite_tac[state_array_to_string_compute]
+  \\ qmatch_goalsub_abbrev_tac`5 * 5 * sw`
+  \\ `sw = s.w` by rw[Abbr`sw`]
+  \\ qunabbrev_tac`sw` \\ pop_assum SUBST_ALL_TAC
+  \\ qmatch_goalsub_abbrev_tac`GENLIST f n`
+  \\ `LENGTH pi_w64_indices = 25`
+     by rewrite_tac[pi_w64_indices_def, LENGTH_GENLIST]
+  \\ simp[LIST_EQ_REWRITE]
+  \\ conj_asm1_tac
+  >- (
+    DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ simp[NULL_LENGTH]
+    \\ rw[Abbr`n`, divides_def, bool_to_bit_def] )
+  \\ rpt strip_tac
+  \\ DEP_REWRITE_TAC[EL_MAP]
+  \\ simp[]
+  \\ `LENGTH (chunks 64 (MAP bool_to_bit bs)) = 25`
+  by (
+    DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ simp[NULL_LENGTH]
+    \\ simp[bool_to_bit_def, divides_def]
+    \\ strip_tac \\ gs[] )
+  \\ conj_asm1_tac >- (
+    mp_tac pi_w64_indices_bound
+    \\ simp[EVERY_MEM, MEM_EL, PULL_EXISTS]
+    \\ disch_then drule \\ simp[] )
+  \\ AP_TERM_TAC
+  \\ DEP_REWRITE_TAC[EL_chunks]
+  \\ simp[NULL_LENGTH]
+  \\ conj_asm1_tac >- ( rw[Abbr`n`] \\ strip_tac \\ gs[] )
+  \\ simp[LIST_EQ_REWRITE, LENGTH_TAKE_EQ]
+  \\ reverse IF_CASES_TAC
+  >- ( pop_assum mp_tac \\ simp[Abbr`n`] )
+  \\ simp[] \\ qx_gen_tac`i` \\ strip_tac
+  \\ DEP_REWRITE_TAC[EL_TAKE, EL_DROP, EL_MAP, EL_GENLIST]
+  \\ simp[] \\ AP_TERM_TAC
+  \\ simp[Abbr`f`, restrict_def, DIV_LT_X]
+  \\ ` i DIV 64 = 0` by simp[DIV_EQ_0]
+  \\ rw[string_to_state_array_def, restrict_def, b2w_def]
+  \\ AP_THM_TAC \\ AP_TERM_TAC
+  \\ rewrite_tac[pi_w64_indices_def]
+  \\ DEP_REWRITE_TAC[EL_GENLIST]
+  \\ simp[]
+QED
+
 (*
 TODO: define Rnd w64 version
 TODO: define (Keccak_p 24) w64 version
@@ -3260,9 +3345,12 @@ Keccak_def
 sponge_def
 Keccak_p_def
 Rnd_def
-pi_def
 chi_def
 iota_compute
+
+Definition iota_w64_def:
+  iota_w64 i (s: word64 list) =
+
 *)
 
 Definition Keccak_256_bytes_def:

From 642afd380428408189895ad6e4ac3d7cd03a5905 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Thu, 12 Dec 2024 17:58:00 +0000
Subject: [PATCH 15/27] Start on chi_w64

---
 examples/Crypto/Keccak/keccakScript.sml | 181 +++++++++++++++++++++++-
 1 file changed, 180 insertions(+), 1 deletion(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 1801be45d9..8cb1795eb7 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -2,7 +2,8 @@ open HolKernel Parse boolLib bossLib dep_rewrite blastLib
      bitLib reduceLib combinLib optionLib sptreeLib wordsLib computeLib;
 open optionTheory pairTheory arithmeticTheory combinTheory listTheory
      rich_listTheory whileTheory bitTheory dividesTheory wordsTheory
-     numposrepTheory numeral_bitTheory logrootTheory sptreeTheory;
+     indexedListsTheory numposrepTheory numeral_bitTheory
+     logrootTheory sptreeTheory;
 
 (* The SHA-3 Standard: https://doi.org/10.6028/NIST.FIPS.202 *)
 
@@ -95,6 +96,15 @@ Proof
   \\ simp[LASTN_DROP, BUTLASTN_TAKE]
 QED
 
+(*
+Theorem word_from_bin_list_and:
+  LENGTH l1 = LENGTH l2 ==>
+  word_from_bin_list l1 && word_from_bin_list l2 =
+  word_from_bin_list (MAP2 (\x y. if (ODD x) /\ (ODD y) then 1 else 0) l1 l2)
+Proof
+  rw[word_from_bin_list_def, l2w_def, word_and_n2w]
+  *)
+
 Theorem chunks_append_divides:
   ∀n l1 l2.
     0 < n /\ divides n (LENGTH l1) /\ ~NULL l1 /\ ~NULL l2 ==>
@@ -309,6 +319,109 @@ Proof
   \\ simp[]
 QED
 
+Theorem l2n_max:
+  0 < b ==>
+  !ls. (l2n b ls = b ** (LENGTH ls) - 1) <=>
+       (EVERY ((=) (b - 1) o flip $MOD b) ls)
+Proof
+  strip_tac
+  \\ Induct
+  \\ rw[l2n_def]
+  \\ rw[EXP]
+  \\ qmatch_goalsub_abbrev_tac`b * l + a`
+  \\ qmatch_goalsub_abbrev_tac`b ** n`
+  \\ gs[EQ_IMP_THM]
+  \\ conj_tac
+  >- (
+    strip_tac
+    \\ Cases_on`n=0` \\ gs[] >- gs[Abbr`n`]
+    \\ `0 < b * b ** n` by simp[]
+    \\ `a + b * l + 1 = b * b ** n` by simp[]
+    \\ `(b * b ** n) DIV b = b ** n` by simp[MULT_TO_DIV]
+    \\ `(b * l + (a + 1)) DIV b = b ** n` by gs[]
+    \\ `(b * l) MOD b = 0` by simp[]
+    \\ `(b * l + (a + 1)) DIV b = (b * l) DIV b + (a + 1) DIV b`
+    by ( irule ADD_DIV_RWT \\ simp[] )
+    \\ pop_assum SUBST_ALL_TAC
+    \\ `(a + 1) DIV b = if a = b - 1 then 1 else 0`
+    by (
+      rw[]
+      \\ `a + 1 < b` suffices_by rw[DIV_EQ_0]
+      \\ simp[Abbr`a`]
+      \\ `h MOD b < b - 1` suffices_by simp[]
+      \\ `h MOD b < b` by simp[]
+      \\ gs[] )
+    \\ `b * l DIV b = l` by simp[MULT_TO_DIV]
+    \\ pop_assum SUBST_ALL_TAC
+    \\ pop_assum SUBST_ALL_TAC
+    \\ `l < b ** n` by ( qunabbrev_tac`l` \\ qunabbrev_tac`n`
+                         \\ irule l2n_lt \\ simp[] )
+    \\ Cases_on`a = b - 1` \\ gs[] )
+  \\ strip_tac
+  \\ rewrite_tac[LEFT_SUB_DISTRIB]
+  \\ qpat_x_assum`_ = a`(SUBST1_TAC o SYM)
+  \\ gs[SUB_LEFT_ADD] \\ rw[]
+  \\ Cases_on`n=0` \\ gs[]
+  \\ `b ** n <= b ** 0` by simp[]
+  \\ gs[EXP_BASE_LE_IFF]
+QED
+
+Theorem l2n_2_neg:
+  !ls.
+  EVERY ($> 2) ls ==>
+  2 ** LENGTH ls - SUC (l2n 2 ls) = l2n 2 (MAP (\x. 1 - x) ls)
+Proof
+  Induct
+  \\ rw[l2n_def]
+  \\ gs[EXP, ADD1]
+  \\ first_x_assum(CHANGED_TAC o SUBST1_TAC o SYM)
+  \\ simp[LEFT_SUB_DISTRIB, LEFT_ADD_DISTRIB, SUB_RIGHT_ADD]
+  \\ qspecl_then[`ls`,`2`]mp_tac l2n_lt
+  \\ simp[]
+QED
+
+Theorem word_not_bits:
+  LENGTH ls = dimindex(:'a) /\ EVERY ($> 2) ls ==>
+  ¬word_from_bin_list ls : 'a word =
+  word_from_bin_list (MAP (λx. 1 - x) ls)
+Proof
+  rw[word_from_bin_list_def, l2w_def]
+  \\ rewrite_tac[word_2comp_n2w]
+  \\ Cases_on`l2n 2 ls = dimword(:'a) - 1`
+  >- (
+    mp_then Any (qspec_then`ls`mp_tac)
+      l2n_max (SIMP_CONV(srw_ss())[]``0 < 2n`` |> EQT_ELIM)
+    \\ `dimword (:'a) = 2 ** LENGTH ls` by simp[dimword_def]
+    \\ first_assum (SUBST_ALL_TAC o SYM)
+    \\ pop_assum kall_tac
+    \\ pop_assum SUBST_ALL_TAC
+    \\ simp[ADD1, ZERO_LT_dimword]
+    \\ strip_tac
+    \\ qmatch_goalsub_abbrev_tac`A MOD N = 0`
+    \\ `A = 0` suffices_by rw[]
+    \\ rw[Abbr`A`, l2n_eq_0]
+    \\ gs[EVERY_MAP, EVERY_MEM]
+    \\ rw[]
+    \\ `2 > x` by simp[]
+    \\ `x < 2` by simp[]
+    \\ pop_assum mp_tac
+    \\ `x MOD 2 = 1` by simp[]
+    \\ rewrite_tac[NUMERAL_LESS_THM]
+    \\ strip_tac \\ fs[] )
+  \\ `SUC (l2n 2 ls) < dimword(:'a)`
+  by (
+    qspecl_then[`ls`,`2`]mp_tac l2n_lt
+    \\ gs[dimword_def] )
+  \\ qmatch_goalsub_abbrev_tac`_ = n2w $ l2n 2 l1`
+  \\ `l2n 2 l1 < dimword(:'a)`
+  by (
+    qspecl_then[`l1`,`2`]mp_tac l2n_lt
+    \\ gs[dimword_def, Abbr`l1`] )
+  \\ simp[Abbr`l1`]
+  \\ drule l2n_2_neg
+  \\ simp[dimword_def]
+QED
+
 Theorem concat_word_list_bytes_to_64:
   LENGTH (ls: word8 list) = 8 ⇒
   concat_word_list ls : word64 =
@@ -3336,6 +3449,72 @@ Proof
   \\ simp[]
 QED
 
+Definition chi_w64_def:
+  chi_w64 (s: word64 list) =
+  MAPi (λi w. let y = 5 * (i DIV 5) in
+    w ?? (~(EL (y + ((i + 1) MOD 5)) s) &&
+           (EL (y + ((i + 2) MOD 5)) s))) s
+End
+
+(*
+Theorem chi_w64_thm:
+  state_bools_w64 bs ws ∧
+  string_to_state_array bs = s ⇒
+  state_bools_w64 (state_array_to_string (chi s)) (chi_w64 ws)
+Proof
+  strip_tac
+  \\ gs[state_bools_w64_def]
+  \\ conj_asm1_tac >- rw[string_to_state_array_def, b2w_def]
+  \\ simp[chi_def, chi_w64_def]
+  \\ rewrite_tac[state_array_to_string_compute]
+  \\ qmatch_goalsub_abbrev_tac`5 * 5 * sw`
+  \\ `sw = s.w` by rw[Abbr`sw`]
+  \\ qunabbrev_tac`sw` \\ pop_assum SUBST_ALL_TAC
+  \\ qmatch_goalsub_abbrev_tac`GENLIST f n`
+  \\ simp[MAPi_GENLIST]
+  \\ `LENGTH (chunks 64 (MAP bool_to_bit bs)) = 25`
+  by (
+    DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ simp[NULL_LENGTH]
+    \\ simp[bool_to_bit_def, divides_def]
+    \\ strip_tac \\ gs[] )
+  \\ qmatch_assum_abbrev_tac`m = 25`
+  \\ simp[LIST_EQ_REWRITE]
+  \\ `bs <> []` by (strip_tac \\ gs[])
+  \\ `n <> 0` by gs[Abbr`n`]
+  \\ conj_asm1_tac
+  >- (
+    DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ simp[NULL_LENGTH]
+    \\ simp[bool_to_bit_def, divides_def, Abbr`n`] )
+  \\ rpt strip_tac
+  \\ DEP_REWRITE_TAC[EL_MAP]
+  \\ simp[]
+  \\ `x DIV 5 < 5` by simp[DIV_LT_X]
+  \\ `5 * (x DIV 5) <= 20` by simp[]
+  \\ simp[]
+  \\ conj_asm1_tac
+  >- (
+    `25 = 20 + 5` by simp[]
+    \\ pop_assum SUBST1_TAC
+    \\ conj_tac
+    \\ irule LESS_EQ_LESS_TRANS
+    \\ qmatch_goalsub_abbrev_tac`_ + y <= _`
+    \\ qexists_tac`20 + y`
+    \\ (reverse conj_tac >- simp[])
+    \\ rewrite_tac[LT_ADD_LCANCEL]
+    \\ simp[Abbr`y`] )
+  \\ DEP_REWRITE_TAC[word_not_bits, EL_chunks]
+  \\ simp[NULL_LENGTH]
+  \\ conj_tac
+  >- (
+    irule EVERY_TAKE
+    \\ irule EVERY_DROP
+    \\ simp[EVERY_MAP, bool_to_bit_def]
+    \\ rw[EVERY_MEM] \\ rw[] )
+  \\
+*)
+
 (*
 TODO: define Rnd w64 version
 TODO: define (Keccak_p 24) w64 version

From 6015c407815b6a724efda76d251b83933b400706 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Thu, 12 Dec 2024 19:09:15 +0000
Subject: [PATCH 16/27] Prove chi_w64_thm

---
 examples/Crypto/Keccak/keccakScript.sml | 122 +++++++++++++++++++++---
 1 file changed, 109 insertions(+), 13 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 8cb1795eb7..a31f3d852a 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -11,6 +11,10 @@ val _ = new_theory "keccak";
 
 val _ = numLib.temp_prefer_num();
 
+Definition bool_to_bit_def:
+  bool_to_bit b = if b then 1 else 0n
+End
+
 Theorem GENLIST_EQ_NIL[simp]:
   GENLIST f n = [] <=> n = 0
 Proof
@@ -38,6 +42,13 @@ Proof
   rw[SBIT_def, ODD_EXP_IFF]
 QED
 
+Theorem ODD_bool_to_bit[simp]:
+  ODD (bool_to_bit b) = b /\
+  ODD (1 - bool_to_bit b) = ~b
+Proof
+  rw[bool_to_bit_def]
+QED
+
 Theorem LENGTH_word_to_bin_list_bound:
   LENGTH (word_to_bin_list (w:'a word)) <= (dimindex (:'a))
 Proof
@@ -96,14 +107,73 @@ Proof
   \\ simp[LASTN_DROP, BUTLASTN_TAKE]
 QED
 
-(*
-Theorem word_from_bin_list_and:
+Theorem ODD_MOD_2[simp]:
+  ODD (x MOD 2) = ODD x
+Proof
+  rw[ODD_MOD2_LEM]
+QED
+
+Theorem bool_to_bit_MOD_2[simp]:
+  bool_to_bit x MOD 2 = bool_to_bit x
+Proof
+  rw[bool_to_bit_def]
+QED
+
+Theorem MOD_DIV_SAME[simp]:
+  0 < y ==> x MOD y DIV y = 0
+Proof
+  strip_tac
+  \\ Cases_on`y=1` \\ gs[]
+  \\ `1 < y` by simp[]
+  \\ rw[DIV_EQ_0]
+QED
+
+Theorem BITWISE_l2n_2:
   LENGTH l1 = LENGTH l2 ==>
-  word_from_bin_list l1 && word_from_bin_list l2 =
-  word_from_bin_list (MAP2 (\x y. if (ODD x) /\ (ODD y) then 1 else 0) l1 l2)
+  BITWISE (LENGTH l1) op (l2n 2 l1) (l2n 2 l2) =
+  l2n 2 (MAP2 (\x y. bool_to_bit $ op (ODD x) (ODD y)) l1 l2)
+Proof
+  qid_spec_tac`l2`
+  \\ Induct_on`l1`
+  \\ simp[BITWISE_EVAL]
+  >- simp[BITWISE_def]
+  \\ qx_gen_tac`b`
+  \\ Cases \\ gs[BITWISE_EVAL]
+  \\ strip_tac
+  \\ gs[l2n_def]
+  \\ simp[SBIT_def, ODD_ADD, ODD_MULT, GSYM bool_to_bit_def]
+QED
+
+Theorem word_from_bin_list_and:
+  LENGTH l1 = dimindex(:'a) /\
+  LENGTH l2 = dimindex(:'a)
+  ==>
+  word_from_bin_list l1 && word_from_bin_list l2 : 'a word =
+  word_from_bin_list (MAP2 (\x y. bool_to_bit $ (ODD x /\ ODD y)) l1 l2)
 Proof
   rw[word_from_bin_list_def, l2w_def, word_and_n2w]
-  *)
+  \\ qmatch_goalsub_abbrev_tac`BITWISE n`
+  \\ qmatch_goalsub_abbrev_tac`a MOD d = b MOD d`
+  \\ `d = 2 ** n`
+  by simp[Abbr`d`, Abbr`n`, dimword_def]
+  \\ `a < d` by (
+    pop_assum SUBST1_TAC
+    \\ qunabbrev_tac`a`
+    \\ irule BITWISE_LT_2EXP )
+  \\ `b < d`
+  by (
+    qunabbrev_tac`b`
+    \\ qmatch_goalsub_abbrev_tac`l2n 2 ls`
+    \\ `n = LENGTH ls` by simp[Abbr`ls`]
+    \\ qunabbrev_tac`d`
+    \\ qpat_x_assum`_ = 2 ** _`SUBST1_TAC
+    \\ pop_assum SUBST1_TAC
+    \\ irule l2n_lt \\ simp[] )
+  \\ simp[]
+  \\ unabbrev_all_tac
+  \\ DEP_REWRITE_TAC[GSYM BITWISE_l2n_2]
+  \\ simp[]
+QED
 
 Theorem chunks_append_divides:
   ∀n l1 l2.
@@ -156,10 +226,6 @@ Proof
   \\ Cases_on`b` \\ gs[MULT]
 QED
 
-Definition bool_to_bit_def:
-  bool_to_bit b = if b then 1 else 0
-End
-
 Theorem LENGTH_chunks:
   ∀n ls. 0 < n ∧ ¬NULL ls ⇒
     LENGTH (chunks n ls) =
@@ -3456,7 +3522,6 @@ Definition chi_w64_def:
            (EL (y + ((i + 2) MOD 5)) s))) s
 End
 
-(*
 Theorem chi_w64_thm:
   state_bools_w64 bs ws ∧
   string_to_state_array bs = s ⇒
@@ -3512,8 +3577,40 @@ Proof
     \\ irule EVERY_DROP
     \\ simp[EVERY_MAP, bool_to_bit_def]
     \\ rw[EVERY_MEM] \\ rw[] )
-  \\
-*)
+  \\ DEP_REWRITE_TAC[word_from_bin_list_and]
+  \\ simp[]
+  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ simp[]
+  \\ AP_TERM_TAC
+  \\ simp[LIST_EQ_REWRITE, LENGTH_TAKE_EQ]
+  \\ conj_tac >- rw[Abbr`n`]
+  \\ qx_gen_tac`i` \\ strip_tac
+  \\ simp[EL_MAP, EL_TAKE, EL_ZIP, EL_MAP2]
+  \\ DEP_REWRITE_TAC[EL_DROP]
+  \\ simp[]
+  \\ conj_tac >- rw[Abbr`n`]
+  \\ simp[EL_MAP]
+  \\ DEP_REWRITE_TAC[EL_MAP, EL_GENLIST]
+  \\ conj_tac >- rw[Abbr`n`]
+  \\ simp[Abbr`f`, restrict_def]
+  \\ qpat_x_assum`LENGTH _ = 25`kall_tac
+  \\ rw[string_to_state_array_def, restrict_def, b2w_def, DIV_LT_X]
+  \\ `i DIV 64 = 0` by simp[DIV_EQ_0]
+  \\ simp[]
+  \\ qmatch_goalsub_abbrev_tac`c <> (~a ∧ b)`
+  \\ `c = EL (i + 64 * x) bs`
+  by (
+    simp[Abbr`c`]
+    \\ AP_THM_TAC \\ AP_TERM_TAC
+    \\ AP_TERM_TAC
+    \\ AP_TERM_TAC
+    \\ qspec_then`5`mp_tac DIVISION
+    \\ impl_tac >- rw[]
+    \\ disch_then(qspec_then`x`mp_tac)
+    \\ simp[] )
+  \\ simp[Abbr`c`]
+  \\ rw[bool_to_bit_def]
+QED
 
 (*
 TODO: define Rnd w64 version
@@ -3524,7 +3621,6 @@ Keccak_def
 sponge_def
 Keccak_p_def
 Rnd_def
-chi_def
 iota_compute
 
 Definition iota_w64_def:

From 1819c6eb2989fcdc419e027a3df32f1fc9970017 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Thu, 12 Dec 2024 22:42:50 +0000
Subject: [PATCH 17/27] Start on iota_w64

---
 examples/Crypto/Keccak/keccakScript.sml | 184 +++++++++++++++++++++++-
 1 file changed, 180 insertions(+), 4 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index a31f3d852a..e09c3ebdc4 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -209,6 +209,14 @@ Proof
   rw[Once chunks_def]
 QED
 
+Theorem chunks_not_nil[simp]:
+  !n ls. chunks n ls <> []
+Proof
+  recInduct chunks_ind
+  \\ rw[]
+  \\ rw[Once chunks_def]
+QED
+
 Theorem MEM_w2l_less:
   1 < b /\ MEM x (w2l b w) ==> x < b
 Proof
@@ -317,6 +325,17 @@ Proof
   \\ gs[LT_EXP_LOG]
 QED
 
+Theorem LENGTH_PAD_RIGHT_0_64_word_to_bin_list[simp]:
+  LENGTH (PAD_RIGHT 0 64 (word_to_bin_list (w: word64))) = 64
+Proof
+  rw[word_to_bin_list_def, wordsTheory.w2l_def, PAD_RIGHT, LENGTH_n2l, LOG2_def]
+  \\ Cases_on`w` \\ gs[]
+  \\ rewrite_tac[Once ADD_SYM]
+  \\ irule SUB_ADD
+  \\ `n < 2 ** 64` by simp[]
+  \\ gs[LT_EXP_LOG]
+QED
+
 Theorem l2n_PAD_RIGHT_0[simp]:
   0 < b ==> l2n b (PAD_RIGHT 0 h ls) = l2n b ls
 Proof
@@ -325,6 +344,12 @@ Proof
   \\ gs[l2n_eq_0, EVERY_GENLIST]
 QED
 
+Theorem l2w_PAD_RIGHT_0[simp]:
+  0 < b ==> l2w b (PAD_RIGHT 0 h ls) = l2w b ls
+Proof
+  rw[l2w_def]
+QED
+
 Theorem BITWISE_COMM:
   (!m. m <= n ==> op (BIT m x) (BIT m y) = op (BIT m y) (BIT m x))
   ==> BITWISE n op x y = BITWISE n op y x
@@ -3612,6 +3637,161 @@ Proof
   \\ rw[bool_to_bit_def]
 QED
 
+Definition iota_w64_RCz_def:
+  iota_w64_RCz : word64 list = MAP n2w [
+                      1;               32898;
+    9223372036854808714; 9223372039002292224;
+                  32907;          2147483649;
+    9223372039002292353; 9223372036854808585;
+                    138;                 136;
+             2147516425;          2147483658;
+             2147516555; 9223372036854775947;
+    9223372036854808713; 9223372036854808579;
+    9223372036854808578; 9223372036854775936;
+                  32778; 9223372039002259466;
+    9223372039002292353; 9223372036854808704;
+             2147483649; 9223372039002292232
+  ]
+End
+
+Definition iota_w64_def:
+  iota_w64 (s: word64 list) c =
+  case s of [] => [] | h :: t => (c ?? h) :: t
+End
+
+Theorem iota_w64_thm:
+  state_bools_w64 bs ws ∧
+  string_to_state_array bs = s ∧
+  i < 24
+  ⇒
+  state_bools_w64 (state_array_to_string (iota s i))
+    (iota_w64 ws (EL i iota_w64_RCz))
+Proof
+  strip_tac
+  \\ gs[state_bools_w64_def]
+  \\ conj_asm1_tac >- rw[string_to_state_array_def, b2w_def]
+  \\ simp[iota_def, iota_w64_def]
+  \\ rewrite_tac[state_array_to_string_compute]
+  \\ qmatch_goalsub_abbrev_tac`5 * 5 * sw`
+  \\ `sw = s.w` by rw[Abbr`sw`]
+  \\ qunabbrev_tac`sw` \\ pop_assum SUBST_ALL_TAC
+  \\ qmatch_goalsub_abbrev_tac`GENLIST f n`
+  \\ CASE_TAC >- gs[]
+  \\ simp[Once chunks_def]
+  \\ IF_CASES_TAC >- gs[Abbr`n`]
+  \\ simp[]
+  \\ qmatch_goalsub_abbrev_tac`t = MAP _ lg`
+  \\ `LENGTH lg = 24`
+  by (
+    simp[Abbr`lg`]
+    \\ DEP_REWRITE_TAC[LENGTH_chunks]
+    \\ simp[NULL_LENGTH]
+    \\ rw[bool_to_bit_def, divides_def, Abbr`n`] )
+  \\ reverse conj_tac
+  >- (
+    BasicProvers.VAR_EQ_TAC
+    \\ qpat_x_assum`_ = h::t`mp_tac
+    \\ simp[Once chunks_def]
+    \\ rw[]
+    \\ simp[LIST_EQ_REWRITE]
+    \\ conj_asm1_tac
+    >- (
+      DEP_REWRITE_TAC[LENGTH_chunks]
+      \\ simp[NULL_LENGTH]
+      \\ rw[bool_to_bit_def, divides_def, Abbr`n`] )
+    \\ simp[EL_MAP] \\ rw[Abbr`lg`]
+    \\ AP_TERM_TAC
+    \\ DEP_REWRITE_TAC[EL_chunks]
+    \\ simp[NULL_EQ]
+    \\ simp[LIST_EQ_REWRITE, LENGTH_TAKE_EQ]
+    \\ reverse IF_CASES_TAC >- (
+      `F` suffices_by rw[]
+      \\ pop_assum mp_tac
+      \\ rw[Abbr`n`] )
+    \\ simp[EL_TAKE, EL_DROP, EL_MAP]
+    \\ qx_gen_tac`j` \\ strip_tac
+    \\ simp[Abbr`f`, restrict_def, DIV_LT_X]
+    \\ simp[string_to_state_array_def, restrict_def, b2w_def]
+    \\ simp[DIV_LT_X]
+    \\ `j DIV 64 = 0` by simp[DIV_EQ_0]
+    \\ IF_CASES_TAC
+    >- (
+      pop_assum mp_tac
+      \\ simp[ADD_DIV_RWT]
+      \\ simp[DIV_EQ_0]
+      \\ Cases_on`x=0` \\ simp[]
+      \\ Cases_on`x=1` \\ simp[]
+      \\ Cases_on`x=2` \\ simp[]
+      \\ Cases_on`x=3` \\ simp[] )
+    \\ AP_TERM_TAC
+    \\ AP_THM_TAC
+    \\ AP_TERM_TAC
+    \\ simp[]
+    \\ simp[ADD_DIV_RWT]
+    \\ qmatch_goalsub_abbrev_tac`5 * (xx DIV 5)`
+    \\ qspec_then`5`mp_tac DIVISION
+    \\ impl_tac >- rw[]
+    \\ disch_then(qspec_then`xx`mp_tac)
+    \\ simp[]
+    \\ disch_then (SUBST1_TAC o SYM)
+    \\ simp[Abbr`xx`] )
+  \\ simp[MAP_GENLIST, TAKE_GENLIST]
+  \\ `MIN 64 n = 64` by simp[Abbr`n`]
+  \\ pop_assum SUBST1_TAC
+  \\ qmatch_goalsub_abbrev_tac`GENLIST _ m`
+  \\ `h = word_from_bin_list (PAD_RIGHT 0 64 $ word_to_bin_list h)`
+  by simp[word_from_bin_list_def, word_to_bin_list_def, l2w_w2l]
+  \\ pop_assum SUBST1_TAC
+  \\ qmatch_goalsub_abbrev_tac`_ ?? g`
+  \\ `g = word_from_bin_list (PAD_RIGHT 0 64 $ word_to_bin_list g)`
+  by simp[word_from_bin_list_def, word_to_bin_list_def, l2w_w2l]
+  \\ pop_assum SUBST1_TAC
+  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ simp[]
+  \\ AP_TERM_TAC
+  \\ BasicProvers.VAR_EQ_TAC
+  \\ qpat_x_assum`_ = h::t`mp_tac
+  \\ simp[Once chunks_def]
+  \\ IF_CASES_TAC >- fs[Abbr`m`]
+  \\ simp[] \\ strip_tac
+  \\ BasicProvers.VAR_EQ_TAC
+  \\ BasicProvers.VAR_EQ_TAC
+  \\ simp[LIST_EQ_REWRITE]
+  \\ conj_tac
+  >- simp[Abbr`m`]
+  \\ qx_gen_tac`z`
+  \\ qmatch_goalsub_abbrev_tac`_ ==> rsh`
+  \\ simp[Abbr`m`] \\ strip_tac
+  \\ qunabbrev_tac`rsh`
+  \\ DEP_REWRITE_TAC[EL_GENLIST, EL_MAP, EL_ZIP]
+  \\ conj_tac >- simp[]
+  \\ simp[]
+  \\ simp[word_to_bin_list_def]
+  \\ simp[word_from_bin_list_def, w2l_l2w]
+  \\ qmatch_goalsub_abbrev_tac`l2n 2 ll MOD xx`
+  \\ qspecl_then[`ll`,`2`]mp_tac l2n_lt
+  \\ simp[Abbr`ll`]
+  \\ strip_tac
+  \\ `z DIV 64 = 0` by simp[DIV_EQ_0]
+  \\ rw[Abbr`f`, restrict_def]
+  \\ rw[string_to_state_array_def, restrict_def, b2w_def]
+  \\ simp[iota_some_elim]
+  \\ DEP_REWRITE_TAC[n2l_l2n]
+  \\ conj_tac
+  >- (
+    simp[]
+    \\ irule EVERY_TAKE
+    \\ simp[EVERY_MAP, EVERY_MEM]
+    \\ rw[bool_to_bit_def] )
+  \\ IF_CASES_TAC
+  >- (
+    pop_assum mp_tac
+    \\ simp[l2n_eq_0]
+    \\ strip_tac
+    \\ cheat )
+  \\ cheat
+QED
+
 (*
 TODO: define Rnd w64 version
 TODO: define (Keccak_p 24) w64 version
@@ -3621,10 +3801,6 @@ Keccak_def
 sponge_def
 Keccak_p_def
 Rnd_def
-iota_compute
-
-Definition iota_w64_def:
-  iota_w64 i (s: word64 list) =
 
 *)
 

From ce5652ee622b8c1bb341a92dbe80dcef25d1888e Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Fri, 13 Dec 2024 05:25:50 +0000
Subject: [PATCH 18/27] Prove iota_w64_thm

---
 examples/Crypto/Keccak/keccakScript.sml | 120 ++++++++++++++++++++++--
 1 file changed, 113 insertions(+), 7 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index e09c3ebdc4..66befd10f0 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -3,7 +3,7 @@ open HolKernel Parse boolLib bossLib dep_rewrite blastLib
 open optionTheory pairTheory arithmeticTheory combinTheory listTheory
      rich_listTheory whileTheory bitTheory dividesTheory wordsTheory
      indexedListsTheory numposrepTheory numeral_bitTheory
-     logrootTheory sptreeTheory;
+     bitstringTheory logrootTheory sptreeTheory;
 
 (* The SHA-3 Standard: https://doi.org/10.6028/NIST.FIPS.202 *)
 
@@ -15,6 +15,35 @@ Definition bool_to_bit_def:
   bool_to_bit b = if b then 1 else 0n
 End
 
+Theorem dropWhile_id:
+ (dropWhile P ls = ls) <=> NULL ls \/ ~P(HD ls)
+Proof
+  Cases_on`ls` \\ rw[dropWhile_def]
+  \\ disch_then(mp_tac o Q.AP_TERM`LENGTH`)
+  \\ qspecl_then[`P`,`t`]mp_tac LENGTH_dropWhile_LESS_EQ
+  \\ simp[]
+QED
+
+Theorem IS_SUFFIX_dropWhile:
+  IS_SUFFIX ls (dropWhile P ls)
+Proof
+  Induct_on`ls`
+  \\ rw[IS_SUFFIX_CONS]
+QED
+
+Theorem LENGTH_dropWhile_id:
+  (LENGTH (dropWhile P ls) = LENGTH ls) <=> (dropWhile P ls = ls)
+Proof
+  rw[EQ_IMP_THM]
+  \\ rw[dropWhile_id]
+  \\ Cases_on`ls` \\ gs[]
+  \\ strip_tac \\ gs[]
+  \\ `IS_SUFFIX t (dropWhile P t)` by simp[IS_SUFFIX_dropWhile]
+  \\ gs[IS_SUFFIX_APPEND]
+  \\ `LENGTH t = LENGTH l + LENGTH (dropWhile P t)` by metis_tac[LENGTH_APPEND]
+  \\ fs[]
+QED
+
 Theorem GENLIST_EQ_NIL[simp]:
   GENLIST f n = [] <=> n = 0
 Proof
@@ -49,6 +78,13 @@ Proof
   rw[bool_to_bit_def]
 QED
 
+Theorem bool_to_bit_neq_add:
+  bool_to_bit (x <> y) =
+  (bool_to_bit x + bool_to_bit y) MOD 2
+Proof
+  rw[bool_to_bit_def]
+QED
+
 Theorem LENGTH_word_to_bin_list_bound:
   LENGTH (word_to_bin_list (w:'a word)) <= (dimindex (:'a))
 Proof
@@ -3659,6 +3695,17 @@ Definition iota_w64_def:
   case s of [] => [] | h :: t => (c ?? h) :: t
 End
 
+Theorem iota_w64_RCz_rc_thm:
+  z < 64 /\ i < 24 ==>
+  EL z (PAD_RIGHT 0 64 (w2l 2 (EL i iota_w64_RCz))) =
+  if z = 2 ** LOG 2 (SUC z) - 1 then
+    bool_to_bit $ rc (7 * i + LOG 2 (SUC z))
+  else 0
+Proof
+  simp_tac std_ss [NUMERAL_LESS_THM]
+  \\ strip_tac \\ rpt BasicProvers.VAR_EQ_TAC \\ EVAL_TAC
+QED
+
 Theorem iota_w64_thm:
   state_bools_w64 bs ws ∧
   string_to_state_array bs = s ∧
@@ -3783,13 +3830,73 @@ Proof
     \\ irule EVERY_TAKE
     \\ simp[EVERY_MAP, EVERY_MEM]
     \\ rw[bool_to_bit_def] )
-  \\ IF_CASES_TAC
-  >- (
-    pop_assum mp_tac
-    \\ simp[l2n_eq_0]
+  \\ simp[Abbr`g`]
+  \\ qmatch_goalsub_abbrev_tac`l2n 2 w`
+  \\ `LOG 2 (SUC z) <= w2l 64`
+  by (
+    rewrite_tac[definition"w2l_def"]
+    \\ reverse IF_CASES_TAC >- rw[]
+    \\ rewrite_tac[LOG2_def]
+    \\ irule LOG2_LE_MONO
+    \\ simp[] )
+  \\ simp[LOG2_def]
+  \\ simp[l2n_eq_0]
+  \\ qmatch_goalsub_abbrev_tac`COND b0`
+  \\ `¬b0 ⇒ LOG 2 (l2n 2 w) = PRE (LENGTH (dropWhile ((=) 0) (REVERSE w)))`
+  by (
+    simp[Abbr`b0`]
     \\ strip_tac
+    \\ DEP_REWRITE_TAC[LOG_l2n_dropWhile]
+    \\ pop_assum mp_tac
+    \\ simp[EXISTS_MEM, PULL_EXISTS, EVERY_MEM]
+    \\ qx_gen_tac`e` \\ strip_tac
+    \\ qexists_tac`e` \\ simp[]
+    \\ reverse conj_asm2_tac
+    >- (
+      rw[Abbr`w`, GSYM MAP_TAKE, MEM_MAP, bool_to_bit_def]
+      \\ rw[] )
+    \\ first_x_assum drule
+    \\ Cases_on`e = 0` \\ gs[] )
+  \\ simp[]
+  \\ qmatch_goalsub_abbrev_tac`PRE m`
+  \\ `¬b0 ⇒ 0 < m`
+  by (
+    rw[Abbr`b0`, Abbr`m`]
+    \\ CCONTR_TAC \\ fs[dropWhile_eq_nil]
+    \\ rw[]
+    \\ ntac 2 (pop_assum mp_tac)
+    \\ simp[EVERY_MEM, EXISTS_MEM, PULL_EXISTS]
+    \\ qx_gen_tac`e` \\ strip_tac
+    \\ qexists_tac`e` \\ simp[]
+    \\ strip_tac \\ fs[] )
+  \\ simp[iffLR SUC_PRE]
+  \\ qmatch_goalsub_abbrev_tac`_ + EL z ww`
+  \\ `ww = w`
+  by (
+    simp[Abbr`ww`, Abbr`w`]
+    \\ simp[LIST_EQ_REWRITE, length_pad_right]
+    \\ conj_asm1_tac
+    >- (
+      IF_CASES_TAC \\ simp[]
+      \\ IF_CASES_TAC \\ fs[]
+      \\ fs[Abbr`b0`]
+      \\ qunabbrev_tac`m`
+      \\ qmatch_goalsub_abbrev_tac`dropWhile P ls`
+      \\ qspecl_then[`P`,`ls`]mp_tac LENGTH_dropWhile_LESS_EQ
+      \\ simp[Abbr`ls`]
+      \\ simp[LESS_OR_EQ]
+      \\ strip_tac \\ gs[] )
+    \\ simp[EL_TAKE, EL_MAP]
+    \\ qx_gen_tac`x` \\ strip_tac
     \\ cheat )
-  \\ cheat
+  \\ fs[Abbr`ww`]
+  \\ simp[Abbr`w`, EL_TAKE, EL_MAP]
+  \\ simp[bool_to_bit_neq_add]
+  \\ AP_THM_TAC \\ AP_TERM_TAC
+  \\ AP_TERM_TAC
+  \\ simp[iota_w64_RCz_rc_thm]
+  \\ rw[bool_to_bit_def]
+  \\ fs[]
 QED
 
 (*
@@ -3801,7 +3908,6 @@ Keccak_def
 sponge_def
 Keccak_p_def
 Rnd_def
-
 *)
 
 Definition Keccak_256_bytes_def:

From d185b387c4998f7518516acf23436d59f4ab4d75 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Fri, 13 Dec 2024 10:58:44 +0000
Subject: [PATCH 19/27] Prove Rnd_w64_thm

---
 examples/Crypto/Keccak/keccakScript.sml | 52 +++++++++++++++++++++++--
 1 file changed, 49 insertions(+), 3 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 66befd10f0..9dd29989e9 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -3702,7 +3702,12 @@ Theorem iota_w64_RCz_rc_thm:
     bool_to_bit $ rc (7 * i + LOG 2 (SUC z))
   else 0
 Proof
-  simp_tac std_ss [NUMERAL_LESS_THM]
+  strip_tac
+  \\ qpat_x_assum`i < _`mp_tac
+  \\ simp_tac std_ss [NUMERAL_LESS_THM]
+  \\ strip_tac \\ rpt BasicProvers.VAR_EQ_TAC \\ EVAL_TAC
+  \\ pop_assum mp_tac
+  \\ simp_tac std_ss [NUMERAL_LESS_THM]
   \\ strip_tac \\ rpt BasicProvers.VAR_EQ_TAC \\ EVAL_TAC
 QED
 
@@ -3899,15 +3904,56 @@ Proof
   \\ fs[]
 QED
 
+Definition Rnd_w64_def:
+  Rnd_w64 s =
+  iota_w64 $
+  chi_w64 $
+  pi_w64 $
+  rho_w64 $
+  theta_w64 s
+End
+
+Theorem Rnd_w64_thm:
+  state_bools_w64 bs ws ∧
+  string_to_state_array bs = s ∧
+  i < 24 ⇒
+  state_bools_w64 (state_array_to_string (Rnd s i))
+    (Rnd_w64 ws (EL i iota_w64_RCz))
+Proof
+  rewrite_tac[Rnd_w64_def, Rnd_def]
+  \\ strip_tac
+  \\ irule iota_w64_thm
+  \\ rw[]
+  \\ qmatch_goalsub_abbrev_tac`string_to_state_array _ = s`
+  \\ qexists_tac`state_array_to_string s`
+  \\ DEP_REWRITE_TAC[state_array_to_string_to_state_array]
+  \\ simp[Abbr`s`]
+  \\ irule chi_w64_thm
+  \\ qmatch_goalsub_abbrev_tac`string_to_state_array _ = s`
+  \\ qexists_tac`state_array_to_string s`
+  \\ DEP_REWRITE_TAC[state_array_to_string_to_state_array]
+  \\ simp[Abbr`s`]
+  \\ irule pi_w64_thm
+  \\ qmatch_goalsub_abbrev_tac`string_to_state_array _ = s`
+  \\ qexists_tac`state_array_to_string s`
+  \\ DEP_REWRITE_TAC[state_array_to_string_to_state_array]
+  \\ simp[Abbr`s`]
+  \\ irule rho_w64_thm
+  \\ qmatch_goalsub_abbrev_tac`string_to_state_array _ = s`
+  \\ qexists_tac`state_array_to_string s`
+  \\ DEP_REWRITE_TAC[state_array_to_string_to_state_array]
+  \\ simp[Abbr`s`]
+  \\ irule theta_w64_thm
+  \\ metis_tac[]
+QED
+
 (*
-TODO: define Rnd w64 version
 TODO: define (Keccak_p 24) w64 version
 
 Keccak_256_def
 Keccak_def
 sponge_def
 Keccak_p_def
-Rnd_def
 *)
 
 Definition Keccak_256_bytes_def:

From 304f6ba6d14a940e46e0b5f2c525a9eea8399648 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Fri, 13 Dec 2024 13:17:22 +0000
Subject: [PATCH 20/27] Prove Keccak_p_24_w64_thm

---
 examples/Crypto/Keccak/keccakScript.sml | 67 +++++++++++++++++++++++--
 1 file changed, 64 insertions(+), 3 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 9dd29989e9..5f063d9255 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -3947,13 +3947,74 @@ Proof
   \\ metis_tac[]
 QED
 
-(*
-TODO: define (Keccak_p 24) w64 version
+Definition Keccak_p_24_w64_def:
+  Keccak_p_24_w64 s =
+  FOLDL Rnd_w64 s iota_w64_RCz
+End
 
+Theorem Keccak_p_24_w64_lemma[local]:
+  state_bools_w64 bs ws /\ i <= 24 ==>
+  state_bools_w64
+    (state_array_to_string $
+     FST $ FUNPOW (λ(a,i). (Rnd a i, SUC i)) i
+     (string_to_state_array bs, 0))
+    (FOLDL Rnd_w64 ws (TAKE i iota_w64_RCz))
+Proof
+  Induct_on`i` \\ rw[]
+  >- (
+    DEP_REWRITE_TAC[GEN_ALL string_to_state_array_to_string]
+    \\ gs[state_bools_w64_def, iota_w64_RCz_def] )
+  \\ gs[FUNPOW_SUC, UNCURRY]
+  \\ `LENGTH iota_w64_RCz = 24` by simp[iota_w64_RCz_def]
+  \\ qmatch_goalsub_abbrev_tac`FOLDL _ ws ls`
+  \\ qmatch_asmsub_abbrev_tac`FOLDL _ ws tl`
+  \\ `ls = SNOC (EL i iota_w64_RCz) tl`
+  by(
+    simp[Abbr`ls`, Abbr`tl`]
+    \\ simp[LIST_EQ_REWRITE, EL_TAKE, EL_APPEND]
+    \\ rw[]
+    \\ `i = x` by gs[]
+    \\ rw[] )
+  \\ pop_assum SUBST1_TAC
+  \\ rewrite_tac[FOLDL_SNOC]
+  \\ qmatch_goalsub_abbrev_tac`Rnd s j`
+  \\ `j = i`
+  by (
+    simp[Abbr`j`]
+    \\ qmatch_goalsub_abbrev_tac`FUNPOW f`
+    \\ `∀n x y. SND (FUNPOW f n (x,y)) = n + y` suffices_by simp[]
+    \\ Induct \\ rw[FUNPOW_SUC]
+    \\ rw[Abbr`f`, UNCURRY] )
+  \\ rw[Abbr`j`]
+  \\ irule Rnd_w64_thm
+  \\ rw[]
+  \\ goal_assum(first_assum o mp_then Any mp_tac)
+  \\ DEP_REWRITE_TAC[state_array_to_string_to_state_array]
+  \\ rw[Abbr`s`]
+  \\ qmatch_goalsub_abbrev_tac`FUNPOW f`
+  \\ `∀n x y. wf_state_array x ==> wf_state_array $ FST (FUNPOW f n (x,y))`
+  suffices_by ( disch_then irule \\ fs[state_bools_w64_def] )
+  \\ Induct \\ rw[FUNPOW_SUC]
+  \\ rw[Abbr`f`, UNCURRY]
+QED
+
+Theorem Keccak_p_24_w64_thm:
+  state_bools_w64 bs ws ⇒
+  state_bools_w64 (Keccak_p 24 bs) (Keccak_p_24_w64 ws)
+Proof
+  rw[Keccak_p_def, Keccak_p_24_w64_def]
+  \\ `LENGTH bs = 1600` by fs[state_bools_w64_def]
+  \\ rw[string_to_state_array_w, b2w_def, definition"w2l_def"]
+  \\ drule Keccak_p_24_w64_lemma
+  \\ disch_then(qspec_then`24`mp_tac)
+  \\ `LENGTH iota_w64_RCz = 24` by simp[iota_w64_RCz_def]
+  \\ simp[TAKE_LENGTH_TOO_LONG]
+QED
+
+(*
 Keccak_256_def
 Keccak_def
 sponge_def
-Keccak_p_def
 *)
 
 Definition Keccak_256_bytes_def:

From a3be6eb1479ef4c6b6627bc94c5ba2f9075f435a Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Fri, 13 Dec 2024 16:37:01 +0000
Subject: [PATCH 21/27] Prove absorb_w64_thm

---
 examples/Crypto/Keccak/keccakScript.sml | 93 +++++++++++++++++++++++++
 1 file changed, 93 insertions(+)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 5f063d9255..2625f03fe6 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -4011,10 +4011,103 @@ Proof
   \\ simp[TAKE_LENGTH_TOO_LONG]
 QED
 
+Definition absorb_w64_def:
+  absorb_w64 Pis =
+  FOLDL (λSi Pi. Keccak_p_24_w64 (MAP2 word_xor Si Pi))
+    (REPLICATE 25 0w) Pis
+End
+
+Theorem absorb_w64_thm:
+  LIST_REL state_bools_w64 bs ws
+  ==>
+  state_bools_w64
+    (FOLDL (λSi Pi. Keccak_p 24 (MAP2 (λx y. x <> y) Si Pi))
+      (REPLICATE 1600 F) bs)
+    (absorb_w64 ws)
+Proof
+  rw[absorb_w64_def]
+  \\ `REPLICATE 25 (0w:word64) =
+      MAP word_from_bin_list
+        (chunks 64 (MAP bool_to_bit (REPLICATE 1600 F)))`
+  by (
+    simp[LIST_EQ_REWRITE]
+    \\ conj_asm1_tac
+    >- (
+      DEP_REWRITE_TAC[LENGTH_chunks]
+      \\ simp[NULL_LENGTH]
+      \\ EVAL_TAC )
+    \\ rw[EL_REPLICATE, EL_MAP]
+    \\ DEP_REWRITE_TAC[EL_chunks]
+    \\ simp[NULL_LENGTH]
+    \\ rw[word_from_bin_list_def, l2w_def]
+    \\ qmatch_goalsub_abbrev_tac`A MOD B = 0`
+    \\ `A = 0` suffices_by rw[]
+    \\ rw[Abbr`A`, l2n_eq_0]
+    \\ irule EVERY_TAKE
+    \\ rw[REPLICATE_GENLIST, bool_to_bit_def] )
+  \\ pop_assum SUBST1_TAC
+  \\ `LENGTH (REPLICATE 1600 F) = 1600` by simp[]
+  \\ pop_assum mp_tac
+  \\ qspec_tac(`REPLICATE 1600 F`,`s0`)
+  \\ pop_assum mp_tac
+  \\ qid_spec_tac`ws`
+  \\ Induct_on`bs` \\ rw[]
+  >- rw[state_bools_w64_def]
+  \\ first_x_assum drule
+  \\ qmatch_goalsub_abbrev_tac`FOLDL _ sh bs`
+  \\ simp[]
+  \\ disch_then(qspec_then`sh`mp_tac)
+  \\ impl_keep_tac
+  >- (
+    simp[Abbr`sh`, LENGTH_Keccak_p]
+    \\ fs[state_bools_w64_def] )
+  \\ qmatch_goalsub_abbrev_tac`state_bools_w64 s1 (FOLDL f h1 ys)`
+  \\ strip_tac
+  \\ qmatch_goalsub_abbrev_tac`FOLDL f h2 ys`
+  \\ `h1 = h2`
+  by (
+    simp[Abbr`h1`,Abbr`h2`, Abbr`f`, Abbr`sh`]
+    \\ qmatch_goalsub_abbrev_tac`Keccak_p_24_w64 ws`
+    \\ qmatch_goalsub_abbrev_tac`Keccak_p 24 hs`
+    \\ `state_bools_w64 hs ws`
+    by (
+      simp[state_bools_w64_def, Abbr`hs`]
+      \\ gs[Abbr`ws`, state_bools_w64_def]
+      \\ simp[LIST_EQ_REWRITE]
+      \\ DEP_REWRITE_TAC[LENGTH_chunks]
+      \\ simp[NULL_LENGTH]
+      \\ conj_tac >- (rpt strip_tac \\ gs[MAP2_MAP, ZIP_EQ_NIL])
+      \\ simp[divides_def, bool_to_bit_def]
+      \\ rpt strip_tac
+      \\ DEP_REWRITE_TAC[EL_MAP2, EL_MAP]
+      \\ simp[]
+      \\ DEP_REWRITE_TAC[LENGTH_chunks]
+      \\ simp[NULL_LENGTH]
+      \\ conj_tac >- (rpt strip_tac \\ gs[MAP2_MAP, ZIP_EQ_NIL])
+      \\ DEP_REWRITE_TAC[EL_chunks]
+      \\ simp[NULL_LENGTH]
+      \\ DEP_REWRITE_TAC[LENGTH_chunks]
+      \\ simp[NULL_LENGTH]
+      \\ conj_tac >- (rpt strip_tac \\ gs[MAP2_MAP, ZIP_EQ_NIL])
+      \\ conj_tac >- (rpt strip_tac \\ gs[MAP2_MAP, ZIP_EQ_NIL])
+      \\ simp[word_xor_bits_neq]
+      \\ AP_TERM_TAC
+      \\ simp[LIST_EQ_REWRITE]
+      \\ rpt strip_tac
+      \\ DEP_REWRITE_TAC[EL_MAP, EL_ZIP, EL_TAKE, EL_DROP, EL_MAP2]
+      \\ simp[GSYM bool_to_bit_neq_add]
+      \\ rw[bool_to_bit_def] \\ gs[] )
+    \\ drule Keccak_p_24_w64_thm
+    \\ rw[state_bools_w64_def] )
+  \\ rw[]
+QED
+
 (*
 Keccak_256_def
 Keccak_def
 sponge_def
+pad10s1_136_w64_sponge_init
+absorb_w64_thm
 *)
 
 Definition Keccak_256_bytes_def:

From 53e43f7e4889110c99f74b27f29da91d7de84fd9 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 12:22:28 +0000
Subject: [PATCH 22/27] Translate Keccak_256_w64

---
 examples/Crypto/Keccak/keccakScript.sml | 406 +++++++++++++++++++++++-
 1 file changed, 394 insertions(+), 12 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 2625f03fe6..a67a85e8d1 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -3,7 +3,8 @@ open HolKernel Parse boolLib bossLib dep_rewrite blastLib
 open optionTheory pairTheory arithmeticTheory combinTheory listTheory
      rich_listTheory whileTheory bitTheory dividesTheory wordsTheory
      indexedListsTheory numposrepTheory numeral_bitTheory
-     bitstringTheory logrootTheory sptreeTheory;
+     bitstringTheory logrootTheory byteTheory sptreeTheory;
+open cv_transLib cvTheory cv_stdTheory;
 
 (* The SHA-3 Standard: https://doi.org/10.6028/NIST.FIPS.202 *)
 
@@ -11,6 +12,25 @@ val _ = new_theory "keccak";
 
 val _ = numLib.temp_prefer_num();
 
+Theorem cv_LEN_add:
+  cv_LEN cv (Num n) =
+  cv_add (Num n) (cv_LEN cv (Num 0))
+Proof
+  qid_spec_tac`n`
+  \\ Induct_on`cv`
+  >- ( rw[Once cv_LEN_def] \\ rw[Once cv_LEN_def] )
+  \\ rewrite_tac[Once cv_LEN_def]
+  \\ simp_tac (srw_ss()) []
+  \\ gen_tac
+  \\ simp_tac std_ss [Once cv_LEN_def, SimpRHS]
+  \\ simp_tac (srw_ss()) []
+  \\ first_assum(qspec_then`n + 1`SUBST1_TAC)
+  \\ first_assum(qspec_then`1`SUBST1_TAC)
+  \\ qmatch_goalsub_abbrev_tac`cv_add _ p`
+  \\ Cases_on`p`
+  \\ simp[]
+QED
+
 Definition bool_to_bit_def:
   bool_to_bit b = if b then 1 else 0n
 End
@@ -350,6 +370,73 @@ Proof
   \\ simp[ZIP_TAKE]
 QED
 
+Theorem chunks_TAKE:
+  !n ls m. divides n m /\ 0 < m ==>
+    chunks n (TAKE m ls) = TAKE (m DIV n) (chunks n ls)
+Proof
+  recInduct chunks_ind \\ rw[]
+  \\ rw[Once chunks_def, SimpRHS]
+  >- (
+    rw[Once chunks_def] \\ gs[LENGTH_TAKE_EQ]
+    \\ gvs[divides_def]
+    \\ qmatch_goalsub_rename_tac`n * m`
+    \\ `n <= n * m` by simp[]
+    \\ DEP_REWRITE_TAC[TAKE_LENGTH_TOO_LONG]
+    \\ simp[MULT_DIV] )
+  >- gs[divides_def]
+  \\ gs[]
+  \\ simp[Once chunks_def, LENGTH_TAKE_EQ]
+  \\ `n <= m` by gs[divides_def]
+  \\ IF_CASES_TAC
+  >- (
+    pop_assum mp_tac \\ rw[]
+    \\ `m = n` by gs[] \\ gvs[] )
+  \\ gs[TAKE_TAKE, DROP_TAKE]
+  \\ first_x_assum(qspec_then`m - n`mp_tac)
+  \\ simp[]
+  \\ impl_keep_tac >- (
+    gs[divides_def]
+    \\ qexists_tac`q - 1`
+    \\ simp[LEFT_SUB_DISTRIB] )
+  \\ rw[]
+  \\ `m DIV n <> 0` by gs[DIV_EQUAL_0]
+  \\ Cases_on`m DIV n` \\ gs[TAKE_TAKE_MIN]
+  \\ `MIN n m = n` by gs[MIN_DEF] \\ rw[]
+  \\ simp[SUB_DIV]
+QED
+
+Definition chunks_tr_aux_def:
+  chunks_tr_aux n ls acc =
+    if LENGTH ls <= SUC n then REVERSE $ ls :: acc
+    else chunks_tr_aux n (DROP (SUC n) ls) (TAKE (SUC n) ls :: acc)
+Termination
+  WF_REL_TAC`measure $ LENGTH o FST o SND`
+  \\ rw[LENGTH_DROP]
+End
+
+Definition chunks_tr_def:
+  chunks_tr n ls = if n = 0 then [ls] else chunks_tr_aux (n - 1) ls []
+End
+
+Theorem chunks_tr_aux_thm:
+  !n ls acc.
+    chunks_tr_aux n ls acc =
+    REVERSE acc ++ chunks (SUC n) ls
+Proof
+  recInduct chunks_tr_aux_ind
+  \\ rw[]
+  \\ rw[Once chunks_tr_aux_def]
+  >- rw[Once chunks_def]
+  \\ simp[Once chunks_def, SimpRHS]
+QED
+
+Theorem chunks_tr_thm:
+  chunks_tr = chunks
+Proof
+  simp[FUN_EQ_THM, chunks_tr_def]
+  \\ Cases \\ rw[chunks_tr_aux_thm]
+QED
+
 Theorem LENGTH_PAD_RIGHT_0_8_word_to_bin_list[simp]:
   LENGTH (PAD_RIGHT 0 8 (word_to_bin_list (w: word8))) = 8
 Proof
@@ -585,6 +672,15 @@ Proof
   \\ simp[]
 QED
 
+(*
+Theorem word_to_bytes_from_bin_list:
+  word_to_bytes (word_from_bin_list ls :'a word) F =
+  MAP word_from_bin_list (chunks 8 (PAD_RIGHT 0 (dimindex(:'a)) ls))
+Proof
+  cheat
+QED
+*)
+
 Datatype:
   state_array =
   <| w: num
@@ -872,7 +968,7 @@ Proof
   rw[chi_def]
 QED
 
-Definition rc_step_def:
+Definition rc_step_def[nocompute]:
   rc_step r =
   let ra = F :: r in
   let re =
@@ -886,6 +982,9 @@ Definition rc_step_def:
     TAKE 8 re
 End
 
+Theorem rc_step_inlined[compute] =
+  “rc_step r” |> SIMP_CONV (srw_ss()) [rc_step_def, LET_THM];
+
 Definition rc_def:
   rc t =
   if t MOD 255 = 0 then T else
@@ -3707,8 +3806,10 @@ Proof
   \\ simp_tac std_ss [NUMERAL_LESS_THM]
   \\ strip_tac \\ rpt BasicProvers.VAR_EQ_TAC \\ EVAL_TAC
   \\ pop_assum mp_tac
-  \\ simp_tac std_ss [NUMERAL_LESS_THM]
-  \\ strip_tac \\ rpt BasicProvers.VAR_EQ_TAC \\ EVAL_TAC
+  \\ CONV_TAC(LAND_CONV(SIMP_CONV std_ss [NUMERAL_LESS_THM]))
+  \\ strip_tac \\ rpt BasicProvers.VAR_EQ_TAC
+  \\ simp_tac (srw_ss()) []
+  \\ EVAL_TAC
 QED
 
 Theorem iota_w64_thm:
@@ -4102,13 +4203,18 @@ Proof
   \\ rw[]
 QED
 
-(*
-Keccak_256_def
-Keccak_def
-sponge_def
-pad10s1_136_w64_sponge_init
-absorb_w64_thm
-*)
+Definition eight_zeros_w64_def:
+  eight_zeros_w64 = [0w; 0w; 0w; 0w; 0w; 0w; 0w; 0w] : word64 list
+End
+
+Definition Keccak_256_w64_def:
+  Keccak_256_w64 bs =
+  FLAT $
+  MAP (flip word_to_bytes F) $
+  TAKE 4 $
+  absorb_w64 $
+  pad10s1_136_w64 eight_zeros_w64 bs []
+End
 
 Definition Keccak_256_bytes_def:
   Keccak_256_bytes (bs:word8 list) : word8 list =
@@ -4118,7 +4224,283 @@ Definition Keccak_256_bytes_def:
     MAP (PAD_RIGHT 0 8 o word_to_bin_list) bs
 End
 
-open cv_transLib cv_stdTheory;
+Theorem Keccak_256_w64_thm:
+  Keccak_256_w64 = Keccak_256_bytes
+Proof
+  simp[Keccak_256_w64_def, Keccak_256_bytes_def, FUN_EQ_THM]
+  \\ qx_gen_tac`bytes`
+  \\ rw[GSYM bytes_to_bools_def]
+  \\ rw[Keccak_256_def, Keccak_def, sponge_def]
+  \\ mp_tac pad10s1_136_w64_sponge_init
+  \\ rw[]
+  \\ `eight_zeros_w64 = REPLICATE 8 0w`
+  by rw[eight_zeros_w64_def, REPLICATE_GENLIST]
+  \\ pop_assum SUBST_ALL_TAC
+  \\ drule absorb_w64_thm \\ strip_tac
+  \\ qmatch_goalsub_abbrev_tac`absorb_w64 sp`
+  \\ qmatch_asmsub_abbrev_tac`state_bools_w64 bs`
+  \\ qmatch_goalsub_abbrev_tac`([], bs1)`
+  \\ `bs1 = bs` by rw[Abbr`bs1`, Abbr`bs`, FOLDL_MAP]
+  \\ gs[Abbr`bs1`] \\ pop_assum kall_tac
+  \\ rw[Once WHILE]
+  \\ rw[Once WHILE]
+  \\ gs[state_bools_w64_def]
+  \\ simp[TAKE_TAKE]
+  \\ simp[GSYM MAP_TAKE, MAP_MAP_o, o_DEF]
+  \\ simp[chunks_MAP, GSYM MAP_TAKE, MAP_MAP_o, o_DEF]
+  \\ DEP_REWRITE_TAC[chunks_TAKE]
+  \\ conj_tac >- rw[divides_def]
+  \\ simp[EVAL``256 DIV 8``]
+  \\ qmatch_goalsub_abbrev_tac`_ = MAP bw _`
+  \\ `bw = word_from_bin_list o MAP bool_to_bit`
+  by rw[bools_to_word_def, FUN_EQ_THM, Abbr`bw`]
+  \\ simp[Abbr`bw`, GSYM MAP_MAP_o]
+  \\ qmatch_goalsub_abbrev_tac`MAP f ls`
+  \\ `f = flip word_to_bytes F o (word_from_bin_list: num list -> word64) o
+          MAP bool_to_bit` by rw[Abbr`f`, FUN_EQ_THM]
+  \\ simp[Abbr`f`, GSYM MAP_MAP_o, Abbr`ls`]
+  \\ simp[MAP_TAKE, GSYM chunks_MAP]
+  \\ cheat
+QED
+
+(* TODO: move/replace *)
+Definition hex_to_rev_bytes_def:
+    hex_to_rev_bytes acc [] = acc : word8 list
+  ∧ hex_to_rev_bytes acc [c] = CONS (n2w (UNHEX c)) acc
+  ∧ hex_to_rev_bytes acc (c1::c2::rest) =
+    hex_to_rev_bytes (CONS (n2w (16 * UNHEX c1 + UNHEX c2)) acc) rest
+End
+
+val () = cv_auto_trans hex_to_rev_bytes_def;
+
+val () = cv_trans_deep_embedding EVAL eight_zeros_w64_def;
+
+val () = cv_auto_trans chunks_tr_aux_def;
+val () = cv_auto_trans chunks_tr_def;
+
+val pad_pre_def = cv_auto_trans_pre (REWRITE_RULE[GSYM chunks_tr_thm]pad10s1_136_w64_def);
+
+Theorem pad10s1_136_w64_pre[cv_pre]:
+  !zs m a. pad10s1_136_w64_pre zs m a
+Proof
+  ho_match_mp_tac pad10s1_136_w64_ind
+  \\ rw[]
+  \\ rw[Once pad_pre_def]
+  \\ gs[chunks_tr_thm]
+QED
+
+Theorem theta_d_w64_inlined:
+  theta_d_w64 s = let
+    a = EL 0 s ?? EL 5 s ?? EL 10 s ?? EL 15 s ?? EL 20 s;
+    b = EL 1 s ?? EL 6 s ?? EL 11 s ?? EL 16 s ?? EL 21 s;
+    c = EL 2 s ?? EL 7 s ?? EL 12 s ?? EL 17 s ?? EL 22 s;
+    d = EL 3 s ?? EL 8 s ?? EL 13 s ?? EL 18 s ?? EL 23 s;
+    e = EL 4 s ?? EL 9 s ?? EL 14 s ?? EL 19 s ?? EL 24 s
+  in
+    [word_rol b 1 ?? e;
+     word_rol c 1 ?? a;
+     word_rol d 1 ?? b;
+     word_rol e 1 ?? c;
+     word_rol a 1 ?? d]
+Proof
+  rw[theta_d_w64_def, theta_c_w64_def]
+QED
+
+Theorem theta_w64_inlined:
+  LENGTH s = 25 ==>
+  theta_w64 s = let
+    a = EL 0 s ?? EL 5 s ?? EL 10 s ?? EL 15 s ?? EL 20 s;
+    b = EL 1 s ?? EL 6 s ?? EL 11 s ?? EL 16 s ?? EL 21 s;
+    c = EL 2 s ?? EL 7 s ?? EL 12 s ?? EL 17 s ?? EL 22 s;
+    d = EL 3 s ?? EL 8 s ?? EL 13 s ?? EL 18 s ?? EL 23 s;
+    e = EL 4 s ?? EL 9 s ?? EL 14 s ?? EL 19 s ?? EL 24 s;
+    j = word_rol b 1 ?? e;
+    k = word_rol c 1 ?? a;
+    l = word_rol d 1 ?? b;
+    m = word_rol e 1 ?? c;
+    n = word_rol a 1 ?? d;
+  in MAP2 $?? s [j;k;l;m;n;j;k;l;m;n;j;k;l;m;n;j;k;l;m;n;j;k;l;m;n]
+Proof
+  CONV_TAC(LAND_CONV(SIMP_CONV std_ss [LENGTH_EQ_NUM_compute]))
+  \\ strip_tac
+  \\ rewrite_tac[theta_w64_def, theta_d_w64_inlined]
+  \\ BasicProvers.LET_ELIM_TAC
+  \\ gvs[Abbr`t`]
+QED
+
+val theta_w64_pre_def = cv_auto_trans_pre (UNDISCH theta_w64_inlined);
+
+Theorem theta_w64_pre:
+  LENGTH s = 25 ==> theta_w64_pre s
+Proof
+  rw[theta_w64_pre_def]
+  \\ strip_tac \\ fs[]
+QED
+
+val rho_w64_pre_def = cv_auto_trans_pre (UNDISCH rho_w64_MAP2);
+
+Theorem rho_w64_pre:
+  LENGTH s = 25 ==> rho_w64_pre s
+Proof
+  rw[rho_w64_pre_def]
+QED
+
+Theorem pi_w64_inlined = SIMP_RULE std_ss [pi_w64_indices_eq, MAP] pi_w64_def;
+
+val pi_w64_pre_def = cv_auto_trans_pre pi_w64_inlined;
+
+Theorem pi_w64_pre:
+  LENGTH s = 25 ==> pi_w64_pre s
+Proof
+  rw[pi_w64_pre_def]
+  \\ strip_tac \\ fs[]
+QED
+
+Theorem chi_w64_inlined:
+  LENGTH s = 25 ==>
+  chi_w64 s = let
+    h00 = EL  0 s; h01 = EL 1  s; h02 = EL  2 s; h03 = EL  3 s; h04 = EL  4 s;
+    h05 = EL  5 s; h06 = EL 6  s; h07 = EL  7 s; h08 = EL  8 s; h09 = EL  9 s;
+    h10 = EL 10 s; h11 = EL 11 s; h12 = EL 12 s; h13 = EL 13 s; h14 = EL 14 s;
+    h15 = EL 15 s; h16 = EL 16 s; h17 = EL 17 s; h18 = EL 18 s; h19 = EL 19 s;
+    h20 = EL 20 s; h21 = EL 21 s; h22 = EL 22 s; h23 = EL 23 s; h24 = EL 24 s;
+  in
+   [h00 ⊕ h02 && ¬h01; h01 ⊕ h03 && ¬h02; h02 ⊕ h04 && ¬h03;
+    h03 ⊕ h00 && ¬h04; h04 ⊕ h01 && ¬h00; h05 ⊕ h07 && ¬h06;
+    h06 ⊕ h08 && ¬h07; h07 ⊕ h09 && ¬h08; h08 ⊕ h05 && ¬h09;
+    h09 ⊕ h06 && ¬h05; h10 ⊕ h12 && ¬h11; h11 ⊕ h13 && ¬h12;
+    h12 ⊕ h14 && ¬h13; h13 ⊕ h10 && ¬h14; h14 ⊕ h11 && ¬h10;
+    h15 ⊕ h17 && ¬h16; h16 ⊕ h18 && ¬h17; h17 ⊕ h19 && ¬h18;
+    h18 ⊕ h15 && ¬h19; h19 ⊕ h16 && ¬h15; h20 ⊕ h22 && ¬h21;
+    h21 ⊕ h23 && ¬h22; h22 ⊕ h24 && ¬h23; h23 ⊕ h20 && ¬h24;
+    h24 ⊕ h21 && ¬h20]
+Proof
+  CONV_TAC(LAND_CONV(SIMP_CONV std_ss [LENGTH_EQ_NUM_compute]))
+  \\ strip_tac
+  \\ rewrite_tac[chi_w64_def]
+  \\ rw[]
+QED
+
+val chi_w64_pre_def = cv_auto_trans_pre (UNDISCH chi_w64_inlined);
+
+Theorem chi_w64_pre:
+  LENGTH s = 25 ==> chi_w64_pre s
+Proof
+  rw[chi_w64_pre_def]
+  \\ strip_tac \\ fs[]
+QED
+
+val () = cv_auto_trans iota_w64_def;
+
+val Rnd_w64_pre_def = cv_auto_trans_pre Rnd_w64_def;
+
+Theorem Rnd_w64_pre:
+  LENGTH s = 25 ==> Rnd_w64_pre s w
+Proof
+  simp[Rnd_w64_pre_def, theta_w64_pre] \\ strip_tac
+  \\ `LENGTH (theta_w64 s) = 25` by simp[theta_w64_inlined]
+  \\ simp[rho_w64_pre]
+  \\ `LENGTH (rho_w64 (theta_w64 s)) = 25` by (
+    simp[rho_w64_MAP2]
+    \\ CASE_TAC \\ fs[]
+    \\ rw[MIN_DEF] )
+  \\ simp[pi_w64_pre]
+  \\ irule chi_w64_pre
+  \\ simp[pi_w64_inlined]
+QED
+
+Theorem Keccak_p_24_w64_inlined =
+  Keccak_p_24_w64_def |> SIMP_RULE std_ss [iota_w64_RCz_def, MAP, FOLDL];
+
+val Keccak_p_24_w64_pre_def = cv_auto_trans_pre Keccak_p_24_w64_inlined;
+
+Definition absorb_w64_rec_def:
+  absorb_w64_rec s [] = s ∧
+  absorb_w64_rec s (Pi::Pis) =
+    absorb_w64_rec (Keccak_p_24_w64 (MAP2 $?? s Pi)) Pis
+End
+
+Theorem absorb_w64_rec_thm:
+  absorb_w64 = absorb_w64_rec (REPLICATE 25 0w)
+Proof
+  simp[FUN_EQ_THM, absorb_w64_def, absorb_w64_rec_def]
+  \\ qspec_tac(`REPLICATE 25 (0w:word64)`,`s`)
+  \\ CONV_TAC SWAP_FORALL_CONV
+  \\ Induct
+  \\ rw[absorb_w64_rec_def]
+QED
+
+val absorb_w64_rec_pre_def = cv_auto_trans_pre absorb_w64_rec_def;
+
+Theorem LENGTH_Rnd_w64:
+  LENGTH s = 25 ==>
+  LENGTH (Rnd_w64 s w) = 25
+Proof
+  rw[Rnd_w64_def]
+  \\ DEP_REWRITE_TAC[theta_w64_inlined]
+  \\ conj_tac >- rw[]
+  \\ BasicProvers.LET_ELIM_TAC
+  \\ DEP_REWRITE_TAC[rho_w64_MAP2]
+  \\ conj_tac >- simp[]
+  \\ CASE_TAC >- gs[LENGTH_EQ_NUM_compute]
+  \\ rewrite_tac[pi_w64_inlined]
+  \\ DEP_REWRITE_TAC[chi_w64_inlined]
+  \\ qmatch_goalsub_abbrev_tac`EL _ zz`
+  \\ conj_tac >- simp[]
+  \\ BasicProvers.LET_ELIM_TAC
+  \\ rewrite_tac[iota_w64_def]
+  \\ simp[]
+QED
+
+Theorem absorb_w64_rec_pre:
+  ∀v s. LENGTH s = 25 /\ EVERY (((=) 25) o LENGTH) v ==> absorb_w64_rec_pre s v
+Proof
+  Induct
+  \\ simp[Once absorb_w64_rec_pre_def]
+  \\ rpt gen_tac \\ strip_tac
+  \\ qmatch_goalsub_abbrev_tac`absorb_w64_rec_pre x`
+  \\ `LENGTH x = 25`
+  by (
+    qunabbrev_tac`x`
+    \\ simp[Keccak_p_24_w64_inlined]
+    \\ DEP_REWRITE_TAC[LENGTH_Rnd_w64]
+    \\ simp[] )
+  \\ rewrite_tac[Keccak_p_24_w64_pre_def]
+  \\ DEP_REWRITE_TAC[Rnd_w64_pre]
+  \\ DEP_REWRITE_TAC[LENGTH_Rnd_w64]
+  \\ simp[]
+QED
+
+val Keccak_256_w64_pre_def = cv_auto_trans_pre $
+  (Keccak_256_w64_def |> SIMP_RULE std_ss [C_DEF, absorb_w64_rec_thm]);
+
+Theorem Keccak_256_w64_pre[cv_pre]:
+  Keccak_256_w64_pre bytes
+Proof
+  rw[Keccak_256_w64_pre_def]
+  \\ irule absorb_w64_rec_pre
+  \\ conj_tac >- rw[]
+  \\ mp_tac pad10s1_136_w64_sponge_init
+  \\ rw[eight_zeros_w64_def]
+  \\ rw[EVERY_MEM, MEM_EL]
+  \\ gs[LIST_REL_EL_EQN]
+  \\ qmatch_goalsub_abbrev_tac`pad10s1_136_w64 r8`
+  \\ `r8 = REPLICATE 8 0w` by simp[Abbr`r8`, REPLICATE_GENLIST]
+  \\ gs[]
+  \\ first_x_assum drule
+  \\ rw[state_bools_w64_def]
+  \\ DEP_REWRITE_TAC[LENGTH_chunks]
+  \\ gs[NULL_LENGTH, divides_def, bool_to_bit_def]
+  \\ strip_tac \\ fs[]
+QED
+
+Theorem Keccak_256_w64_NIL:
+  Keccak_256_w64 [] =
+  REVERSE $ hex_to_rev_bytes []
+  "C5D2460186F7233C927E7DB2DCC703C0E500B653CA82273B7BFAD8045D85A470"
+Proof
+  CONV_TAC cv_eval
+QED
 
 val _ = cv_trans index_to_triple_def;
 val _ = cv_trans triple_to_index_def;

From 6ecfa87eb86e2ce644027794a0013fad88264419 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 12:59:08 +0000
Subject: [PATCH 23/27] Prove a cheat

---
 examples/Crypto/Keccak/keccakScript.sml | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index a67a85e8d1..6a79cb8898 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -3994,7 +3994,30 @@ Proof
       \\ strip_tac \\ gs[] )
     \\ simp[EL_TAKE, EL_MAP]
     \\ qx_gen_tac`x` \\ strip_tac
-    \\ cheat )
+    \\ simp[PAD_RIGHT, EL_GENLIST, EL_APPEND_EQN]
+    \\ Cases_on`b0` \\ gs[]
+    >- (
+      rw[bool_to_bit_def]
+      \\ qhdtm_x_assum`EVERY`mp_tac
+      \\ simp[EXISTS_MEM, MEM_EL, PULL_EXISTS]
+      \\ qexists_tac`x`
+      \\ DEP_REWRITE_TAC[EL_TAKE, EL_MAP]
+      \\ simp[bool_to_bit_def] )
+    \\ DEP_REWRITE_TAC[TAKE_TAKE, LENGTH_TAKE]
+    \\ simp[]
+    \\ conj_asm1_tac
+    >- (
+      reverse conj_asm1_tac >- simp[Abbr`m`]
+      \\ simp[Abbr`m`]
+      \\ qmatch_goalsub_abbrev_tac`dropWhile P ls`
+      \\ qspecl_then[`P`,`ls`]mp_tac LENGTH_dropWhile_LESS_EQ
+      \\ simp[Abbr`ls`] )
+    \\ simp[EL_TAKE, EL_MAP]
+    \\ rw[]
+    \\ fs[NOT_LESS]
+    \\ qunabbrev_tac`m`
+    \\ qpat_x_assum`m <= x`(mp_then Any mp_tac EL_LENGTH_dropWhile_REVERSE)
+    \\ simp[EL_TAKE, EL_MAP])
   \\ fs[Abbr`ww`]
   \\ simp[Abbr`w`, EL_TAKE, EL_MAP]
   \\ simp[bool_to_bit_neq_add]

From 2199455dddc877495c7f20fb03c71a0df8b3f05a Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 18 Dec 2024 12:50:52 +0000
Subject: [PATCH 24/27] Update after upstreaming

---
 examples/Crypto/Keccak/keccakScript.sml | 660 ++----------------------
 1 file changed, 45 insertions(+), 615 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 6a79cb8898..2305a9bd51 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -12,431 +12,6 @@ val _ = new_theory "keccak";
 
 val _ = numLib.temp_prefer_num();
 
-Theorem cv_LEN_add:
-  cv_LEN cv (Num n) =
-  cv_add (Num n) (cv_LEN cv (Num 0))
-Proof
-  qid_spec_tac`n`
-  \\ Induct_on`cv`
-  >- ( rw[Once cv_LEN_def] \\ rw[Once cv_LEN_def] )
-  \\ rewrite_tac[Once cv_LEN_def]
-  \\ simp_tac (srw_ss()) []
-  \\ gen_tac
-  \\ simp_tac std_ss [Once cv_LEN_def, SimpRHS]
-  \\ simp_tac (srw_ss()) []
-  \\ first_assum(qspec_then`n + 1`SUBST1_TAC)
-  \\ first_assum(qspec_then`1`SUBST1_TAC)
-  \\ qmatch_goalsub_abbrev_tac`cv_add _ p`
-  \\ Cases_on`p`
-  \\ simp[]
-QED
-
-Definition bool_to_bit_def:
-  bool_to_bit b = if b then 1 else 0n
-End
-
-Theorem dropWhile_id:
- (dropWhile P ls = ls) <=> NULL ls \/ ~P(HD ls)
-Proof
-  Cases_on`ls` \\ rw[dropWhile_def]
-  \\ disch_then(mp_tac o Q.AP_TERM`LENGTH`)
-  \\ qspecl_then[`P`,`t`]mp_tac LENGTH_dropWhile_LESS_EQ
-  \\ simp[]
-QED
-
-Theorem IS_SUFFIX_dropWhile:
-  IS_SUFFIX ls (dropWhile P ls)
-Proof
-  Induct_on`ls`
-  \\ rw[IS_SUFFIX_CONS]
-QED
-
-Theorem LENGTH_dropWhile_id:
-  (LENGTH (dropWhile P ls) = LENGTH ls) <=> (dropWhile P ls = ls)
-Proof
-  rw[EQ_IMP_THM]
-  \\ rw[dropWhile_id]
-  \\ Cases_on`ls` \\ gs[]
-  \\ strip_tac \\ gs[]
-  \\ `IS_SUFFIX t (dropWhile P t)` by simp[IS_SUFFIX_dropWhile]
-  \\ gs[IS_SUFFIX_APPEND]
-  \\ `LENGTH t = LENGTH l + LENGTH (dropWhile P t)` by metis_tac[LENGTH_APPEND]
-  \\ fs[]
-QED
-
-Theorem GENLIST_EQ_NIL[simp]:
-  GENLIST f n = [] <=> n = 0
-Proof
-  rw[EQ_IMP_THM]
-  \\ pop_assum(mp_tac o Q.AP_TERM`LENGTH`)
-  \\ rewrite_tac[LENGTH_GENLIST]
-  \\ rw[]
-QED
-
-Theorem DIV2_SBIT:
-  DIV2 (SBIT b n) = if n = 0 then 0 else SBIT b (n - 1)
-Proof
-  qspecl_then[`b`,`n`,`1`]mp_tac SBIT_DIV
-  \\ simp[DIV2_def]
-  \\ Cases_on`1 < n` \\ gs[]
-  \\ Cases_on`n=0` \\ gs[SBIT_def]
-  \\ rw[]
-  \\ `n=1` by gs[]
-  \\ gvs[]
-QED
-
-Theorem ODD_SBIT:
-  ODD (SBIT b n) = (b /\ n = 0)
-Proof
-  rw[SBIT_def, ODD_EXP_IFF]
-QED
-
-Theorem ODD_bool_to_bit[simp]:
-  ODD (bool_to_bit b) = b /\
-  ODD (1 - bool_to_bit b) = ~b
-Proof
-  rw[bool_to_bit_def]
-QED
-
-Theorem bool_to_bit_neq_add:
-  bool_to_bit (x <> y) =
-  (bool_to_bit x + bool_to_bit y) MOD 2
-Proof
-  rw[bool_to_bit_def]
-QED
-
-Theorem LENGTH_word_to_bin_list_bound:
-  LENGTH (word_to_bin_list (w:'a word)) <= (dimindex (:'a))
-Proof
-  rw[word_to_bin_list_def, wordsTheory.w2l_def, LENGTH_n2l]
-  \\ Cases_on`w` \\ simp[]
-  \\ fs[dimword_def, GSYM LESS_EQ, LOG2_def, LT_EXP_LOG]
-QED
-
-Theorem word_from_bin_list_ror:
-  x < dimindex(:'a) /\ LENGTH ls = dimindex(:'a)
-  ==>
-  word_ror (word_from_bin_list ls : 'a word) x =
-  word_from_bin_list (DROP x ls ++ TAKE x ls)
-Proof
-  rw[word_from_bin_list_def, l2w_def]
-  \\ Cases_on`x = 0` \\ gs[]
-  \\ rw[word_ror_n2w, l2n_APPEND]
-  \\ AP_THM_TAC \\ AP_TERM_TAC
-  \\ qspecl_then[`x`,`ls`](mp_tac o SYM) TAKE_DROP
-  \\ disch_then(SUBST1_TAC o Q.AP_TERM`l2n 2`)
-  \\ rewrite_tac[l2n_APPEND]
-  \\ simp[]
-  \\ qmatch_goalsub_abbrev_tac`BITS _ _ (2 ** x * ld + lt)`
-  \\ qspecl_then[`x - 1`,`0`,`ld`,`lt`]mp_tac BITS_SUM2
-  \\ simp[ADD1]
-  \\ disch_then kall_tac
-  \\ qspecl_then[`x-1`,`lt`]mp_tac BITS_ZEROL
-  \\ simp[ADD1]
-  \\ impl_keep_tac
-  >- (
-    qspecl_then[`TAKE x ls`,`2`]mp_tac l2n_lt
-    \\ simp[] )
-  \\ simp[]
-  \\ disch_then kall_tac
-  \\ simp_tac std_ss [Once ADD_COMM, SimpRHS]
-  \\ qmatch_goalsub_abbrev_tac`BITS h x`
-  \\ qspecl_then[`h`,`x`,`ld`,`lt`]mp_tac BITS_SUM
-  \\ simp[] \\ disch_then kall_tac
-  \\ DEP_REWRITE_TAC[BITS_ZERO4]
-  \\ simp[Abbr`h`]
-  \\ DEP_REWRITE_TAC[BITS_ZEROL]
-  \\ qspecl_then[`DROP x ls`,`2`]mp_tac l2n_lt
-  \\ simp[ADD1]
-QED
-
-Theorem word_from_bin_list_rol:
-  x < dimindex(:'a) /\ LENGTH ls = dimindex(:'a)
-  ==>
-  word_rol (word_from_bin_list ls : 'a word) x =
-  word_from_bin_list (LASTN x ls ++ BUTLASTN x ls)
-Proof
-  rw[word_rol_def]
-  \\ Cases_on`x=0` \\ gs[]
-  >- simp[LASTN_DROP, BUTLASTN_TAKE, DROP_LENGTH_TOO_LONG, TAKE_LENGTH_TOO_LONG]
-  \\ DEP_REWRITE_TAC[word_from_bin_list_ror]
-  \\ simp[LASTN_DROP, BUTLASTN_TAKE]
-QED
-
-Theorem ODD_MOD_2[simp]:
-  ODD (x MOD 2) = ODD x
-Proof
-  rw[ODD_MOD2_LEM]
-QED
-
-Theorem bool_to_bit_MOD_2[simp]:
-  bool_to_bit x MOD 2 = bool_to_bit x
-Proof
-  rw[bool_to_bit_def]
-QED
-
-Theorem MOD_DIV_SAME[simp]:
-  0 < y ==> x MOD y DIV y = 0
-Proof
-  strip_tac
-  \\ Cases_on`y=1` \\ gs[]
-  \\ `1 < y` by simp[]
-  \\ rw[DIV_EQ_0]
-QED
-
-Theorem BITWISE_l2n_2:
-  LENGTH l1 = LENGTH l2 ==>
-  BITWISE (LENGTH l1) op (l2n 2 l1) (l2n 2 l2) =
-  l2n 2 (MAP2 (\x y. bool_to_bit $ op (ODD x) (ODD y)) l1 l2)
-Proof
-  qid_spec_tac`l2`
-  \\ Induct_on`l1`
-  \\ simp[BITWISE_EVAL]
-  >- simp[BITWISE_def]
-  \\ qx_gen_tac`b`
-  \\ Cases \\ gs[BITWISE_EVAL]
-  \\ strip_tac
-  \\ gs[l2n_def]
-  \\ simp[SBIT_def, ODD_ADD, ODD_MULT, GSYM bool_to_bit_def]
-QED
-
-Theorem word_from_bin_list_and:
-  LENGTH l1 = dimindex(:'a) /\
-  LENGTH l2 = dimindex(:'a)
-  ==>
-  word_from_bin_list l1 && word_from_bin_list l2 : 'a word =
-  word_from_bin_list (MAP2 (\x y. bool_to_bit $ (ODD x /\ ODD y)) l1 l2)
-Proof
-  rw[word_from_bin_list_def, l2w_def, word_and_n2w]
-  \\ qmatch_goalsub_abbrev_tac`BITWISE n`
-  \\ qmatch_goalsub_abbrev_tac`a MOD d = b MOD d`
-  \\ `d = 2 ** n`
-  by simp[Abbr`d`, Abbr`n`, dimword_def]
-  \\ `a < d` by (
-    pop_assum SUBST1_TAC
-    \\ qunabbrev_tac`a`
-    \\ irule BITWISE_LT_2EXP )
-  \\ `b < d`
-  by (
-    qunabbrev_tac`b`
-    \\ qmatch_goalsub_abbrev_tac`l2n 2 ls`
-    \\ `n = LENGTH ls` by simp[Abbr`ls`]
-    \\ qunabbrev_tac`d`
-    \\ qpat_x_assum`_ = 2 ** _`SUBST1_TAC
-    \\ pop_assum SUBST1_TAC
-    \\ irule l2n_lt \\ simp[] )
-  \\ simp[]
-  \\ unabbrev_all_tac
-  \\ DEP_REWRITE_TAC[GSYM BITWISE_l2n_2]
-  \\ simp[]
-QED
-
-Theorem chunks_append_divides:
-  ∀n l1 l2.
-    0 < n /\ divides n (LENGTH l1) /\ ~NULL l1 /\ ~NULL l2 ==>
-    chunks n (l1 ++ l2) = chunks n l1 ++ chunks n l2
-Proof
-  recInduct chunks_ind
-  \\ rw[divides_def, PULL_EXISTS]
-  \\ simp[Once chunks_def]
-  \\ Cases_on`q=0` \\ gs[]
-  \\ IF_CASES_TAC
-  >- ( Cases_on`q` \\ gs[ADD1, LEFT_ADD_DISTRIB] \\ gs[LESS_OR_EQ] )
-  \\ simp[DROP_APPEND, TAKE_APPEND]
-  \\ qmatch_goalsub_abbrev_tac`lhs = _`
-  \\ simp[Once chunks_def]
-  \\ Cases_on`q = 1` \\ gs[]
-  >- (
-    simp[Abbr`lhs`]
-    \\ gs[NOT_LESS_EQUAL]
-    \\ simp[DROP_LENGTH_TOO_LONG])
-  \\ simp[Abbr`lhs`]
-  \\ `n - n * q = 0` by simp[]
-  \\ simp[]
-  \\ first_x_assum irule
-  \\ simp[NULL_EQ]
-  \\ qexists_tac`q - 1`
-  \\ simp[]
-QED
-
-Theorem chunks_length:
-  chunks (LENGTH ls) ls = [ls]
-Proof
-  rw[Once chunks_def]
-QED
-
-Theorem chunks_not_nil[simp]:
-  !n ls. chunks n ls <> []
-Proof
-  recInduct chunks_ind
-  \\ rw[]
-  \\ rw[Once chunks_def]
-QED
-
-Theorem MEM_w2l_less:
-  1 < b /\ MEM x (w2l b w) ==> x < b
-Proof
-  Cases_on`w`
-  \\ rw[wordsTheory.w2l_def]
-  \\ rpt $ pop_assum mp_tac
-  \\ map_every qid_spec_tac [`x`,`n`,`b`]
-  \\ recInduct n2l_ind
-  \\ rw[]
-  \\ pop_assum mp_tac
-  \\ rw[Once n2l_def]
-  >- ( irule MOD_LESS \\ gs[] )
-  \\ first_x_assum irule
-  \\ gs[DIV_LT_X]
-  \\ Cases_on`b` \\ gs[MULT]
-QED
-
-Theorem LENGTH_chunks:
-  ∀n ls. 0 < n ∧ ¬NULL ls ⇒
-    LENGTH (chunks n ls) =
-    LENGTH ls DIV n + (bool_to_bit $ ¬divides n (LENGTH ls))
-Proof
-  recInduct chunks_ind
-  \\ rw[]
-  \\ rw[Once chunks_def, DIV_EQUAL_0, bool_to_bit_def, divides_def]
-  \\ gs[LESS_OR_EQ, ADD1, NULL_EQ, bool_to_bit_def]
-  \\ rw[]
-  \\ gs[divides_def]
-  \\ gs[SUB_DIV]
-  >- (
-    Cases_on`LENGTH ls DIV n = 0` >- gs[DIV_EQUAL_0]
-    \\ simp[] )
-  >- (
-    Cases_on`q` \\ gs[MULT_SUC]
-    \\ qmatch_asmsub_rename_tac`n + n * p`
-    \\ first_x_assum(qspec_then`2 + p`mp_tac)
-    \\ simp[LEFT_ADD_DISTRIB] )
-  >- (
-    first_x_assum(qspec_then`PRE q`mp_tac)
-    \\ Cases_on`q` \\ gs[MULT_SUC] )
-  \\ Cases_on`q` \\ gvs[MULT_SUC]
-  \\ simp[ADD_DIV_RWT]
-QED
-
-Theorem EL_chunks:
-  ∀k ls n.
-  n < LENGTH (chunks k ls) /\ 0 < k /\ ~NULL ls ==>
-  EL n (chunks k ls) = TAKE k (DROP (n * k) ls)
-Proof
-  recInduct chunks_ind \\ rw[NULL_EQ]
-  \\ qpat_x_assum`_ < LENGTH _ `mp_tac
-  \\ rw[Once chunks_def] \\ gs[]
-  >- rw[Once chunks_def]
-  \\ rw[Once chunks_def]
-  \\ qmatch_goalsub_rename_tac`EL m _`
-  \\ Cases_on`m` \\ gs[]
-  \\ pop_assum mp_tac
-  \\ DEP_REWRITE_TAC[LENGTH_chunks]
-  \\ simp[NULL_EQ]
-  \\ strip_tac
-  \\ DEP_REWRITE_TAC[DROP_DROP]
-  \\ simp[MULT_SUC]
-  \\ qmatch_goalsub_rename_tac`n + n * m <= _`
-  \\ `n * m <= LENGTH ls - n` suffices_by simp[]
-  \\ `m <= (LENGTH ls - n) DIV n` suffices_by simp[X_LE_DIV]
-  \\ fs[bool_to_bit_def]
-  \\ pop_assum mp_tac \\ rw[]
-QED
-
-Theorem chunks_MAP:
-  ∀n ls. chunks n (MAP f ls) = MAP (MAP f) (chunks n ls)
-Proof
-  recInduct chunks_ind \\ rw[]
-  \\ rw[Once chunks_def]
-  >- rw[Once chunks_def]
-  >- rw[Once chunks_def]
-  \\ gs[]
-  \\ simp[GSYM MAP_DROP]
-  \\ simp[Once chunks_def, SimpRHS]
-  \\ simp[MAP_TAKE]
-QED
-
-Theorem chunks_ZIP:
-  ∀n ls l2. LENGTH ls = LENGTH l2 ==>
-  chunks n (ZIP (ls, l2)) = MAP ZIP (ZIP (chunks n ls, chunks n l2))
-Proof
-  recInduct chunks_ind \\ rw[]
-  \\ rw[Once chunks_def]
-  >- ( rw[Once chunks_def] \\ rw[Once chunks_def] )
-  >- rw[Once chunks_def]
-  \\ gs[]
-  \\ simp[GSYM ZIP_DROP]
-  \\ simp[Once chunks_def, SimpRHS]
-  \\ simp[Once chunks_def, SimpR``$,``, SimpRHS]
-  \\ simp[ZIP_TAKE]
-QED
-
-Theorem chunks_TAKE:
-  !n ls m. divides n m /\ 0 < m ==>
-    chunks n (TAKE m ls) = TAKE (m DIV n) (chunks n ls)
-Proof
-  recInduct chunks_ind \\ rw[]
-  \\ rw[Once chunks_def, SimpRHS]
-  >- (
-    rw[Once chunks_def] \\ gs[LENGTH_TAKE_EQ]
-    \\ gvs[divides_def]
-    \\ qmatch_goalsub_rename_tac`n * m`
-    \\ `n <= n * m` by simp[]
-    \\ DEP_REWRITE_TAC[TAKE_LENGTH_TOO_LONG]
-    \\ simp[MULT_DIV] )
-  >- gs[divides_def]
-  \\ gs[]
-  \\ simp[Once chunks_def, LENGTH_TAKE_EQ]
-  \\ `n <= m` by gs[divides_def]
-  \\ IF_CASES_TAC
-  >- (
-    pop_assum mp_tac \\ rw[]
-    \\ `m = n` by gs[] \\ gvs[] )
-  \\ gs[TAKE_TAKE, DROP_TAKE]
-  \\ first_x_assum(qspec_then`m - n`mp_tac)
-  \\ simp[]
-  \\ impl_keep_tac >- (
-    gs[divides_def]
-    \\ qexists_tac`q - 1`
-    \\ simp[LEFT_SUB_DISTRIB] )
-  \\ rw[]
-  \\ `m DIV n <> 0` by gs[DIV_EQUAL_0]
-  \\ Cases_on`m DIV n` \\ gs[TAKE_TAKE_MIN]
-  \\ `MIN n m = n` by gs[MIN_DEF] \\ rw[]
-  \\ simp[SUB_DIV]
-QED
-
-Definition chunks_tr_aux_def:
-  chunks_tr_aux n ls acc =
-    if LENGTH ls <= SUC n then REVERSE $ ls :: acc
-    else chunks_tr_aux n (DROP (SUC n) ls) (TAKE (SUC n) ls :: acc)
-Termination
-  WF_REL_TAC`measure $ LENGTH o FST o SND`
-  \\ rw[LENGTH_DROP]
-End
-
-Definition chunks_tr_def:
-  chunks_tr n ls = if n = 0 then [ls] else chunks_tr_aux (n - 1) ls []
-End
-
-Theorem chunks_tr_aux_thm:
-  !n ls acc.
-    chunks_tr_aux n ls acc =
-    REVERSE acc ++ chunks (SUC n) ls
-Proof
-  recInduct chunks_tr_aux_ind
-  \\ rw[]
-  \\ rw[Once chunks_tr_aux_def]
-  >- rw[Once chunks_def]
-  \\ simp[Once chunks_def, SimpRHS]
-QED
-
-Theorem chunks_tr_thm:
-  chunks_tr = chunks
-Proof
-  simp[FUN_EQ_THM, chunks_tr_def]
-  \\ Cases \\ rw[chunks_tr_aux_thm]
-QED
-
 Theorem LENGTH_PAD_RIGHT_0_8_word_to_bin_list[simp]:
   LENGTH (PAD_RIGHT 0 8 (word_to_bin_list (w: word8))) = 8
 Proof
@@ -459,183 +34,6 @@ Proof
   \\ gs[LT_EXP_LOG]
 QED
 
-Theorem l2n_PAD_RIGHT_0[simp]:
-  0 < b ==> l2n b (PAD_RIGHT 0 h ls) = l2n b ls
-Proof
-  Induct_on`ls` \\ rw[l2n_def, PAD_RIGHT, l2n_eq_0, EVERY_GENLIST]
-  \\ gs[PAD_RIGHT, l2n_APPEND]
-  \\ gs[l2n_eq_0, EVERY_GENLIST]
-QED
-
-Theorem l2w_PAD_RIGHT_0[simp]:
-  0 < b ==> l2w b (PAD_RIGHT 0 h ls) = l2w b ls
-Proof
-  rw[l2w_def]
-QED
-
-Theorem BITWISE_COMM:
-  (!m. m <= n ==> op (BIT m x) (BIT m y) = op (BIT m y) (BIT m x))
-  ==> BITWISE n op x y = BITWISE n op y x
-Proof
-  Induct_on`n`
-  \\ rw[BITWISE_def]
-  \\ first_assum(qspec_then`n`mp_tac)
-  \\ impl_tac >- rw[]
-  \\ disch_then SUBST1_TAC
-  \\ simp[]
-  \\ first_x_assum irule
-  \\ rw[]
-  \\ first_x_assum irule
-  \\ simp[]
-QED
-
-Triviality BITWISE_AND_0_lemma:
-  BITWISE w $/\ x 0 = 0
-Proof
-  qid_spec_tac`x`
-  \\ Induct_on`w`
-  \\ rw[BITWISE_def, SBIT_def]
-QED
-
-Theorem BITWISE_AND_0[simp]:
-  BITWISE w $/\ x 0 = 0 /\
-  BITWISE w $/\ 0 x = 0
-Proof
-  qspecl_then[`$/\`,`0`,`x`,`w`]mp_tac(Q.GENL[`op`,`x`,`y`,`n`]BITWISE_COMM)
-  \\ impl_tac >- rw[]
-  \\ disch_then SUBST1_TAC
-  \\ rw[BITWISE_AND_0_lemma]
-QED
-
-Theorem BITWISE_AND_SHIFT_0:
-  !w x y n.
-  x < 2 ** n ==>
-  BITWISE w $/\ x (y * 2 ** n) = 0
-Proof
-  Induct \\ rw[BITWISE_def, SBIT_def]
-  \\ strip_tac
-  \\ Cases_on`w < n`
-  >- ( drule BIT_SHIFT_THM3 \\ simp[]
-       \\ qexists_tac`y` \\ simp[])
-  \\ gs[NOT_LESS]
-  \\ drule TWOEXP_MONO2 \\ strip_tac
-  \\ `x < 2 ** w` by metis_tac[LESS_LESS_EQ_TRANS]
-  \\ drule NOT_BIT_GT_TWOEXP
-  \\ simp[]
-QED
-
-Theorem word_and_lsl_eq_0:
-  w2n w1 < 2 ** n ==> w1 && w2 << n = 0w
-Proof
-  Cases_on`w1` \\ Cases_on`w2`
-  \\ rw[word_and_n2w, word_lsl_n2w]
-  \\ drule BITWISE_AND_SHIFT_0
-  \\ simp[]
-QED
-
-Theorem l2n_max:
-  0 < b ==>
-  !ls. (l2n b ls = b ** (LENGTH ls) - 1) <=>
-       (EVERY ((=) (b - 1) o flip $MOD b) ls)
-Proof
-  strip_tac
-  \\ Induct
-  \\ rw[l2n_def]
-  \\ rw[EXP]
-  \\ qmatch_goalsub_abbrev_tac`b * l + a`
-  \\ qmatch_goalsub_abbrev_tac`b ** n`
-  \\ gs[EQ_IMP_THM]
-  \\ conj_tac
-  >- (
-    strip_tac
-    \\ Cases_on`n=0` \\ gs[] >- gs[Abbr`n`]
-    \\ `0 < b * b ** n` by simp[]
-    \\ `a + b * l + 1 = b * b ** n` by simp[]
-    \\ `(b * b ** n) DIV b = b ** n` by simp[MULT_TO_DIV]
-    \\ `(b * l + (a + 1)) DIV b = b ** n` by gs[]
-    \\ `(b * l) MOD b = 0` by simp[]
-    \\ `(b * l + (a + 1)) DIV b = (b * l) DIV b + (a + 1) DIV b`
-    by ( irule ADD_DIV_RWT \\ simp[] )
-    \\ pop_assum SUBST_ALL_TAC
-    \\ `(a + 1) DIV b = if a = b - 1 then 1 else 0`
-    by (
-      rw[]
-      \\ `a + 1 < b` suffices_by rw[DIV_EQ_0]
-      \\ simp[Abbr`a`]
-      \\ `h MOD b < b - 1` suffices_by simp[]
-      \\ `h MOD b < b` by simp[]
-      \\ gs[] )
-    \\ `b * l DIV b = l` by simp[MULT_TO_DIV]
-    \\ pop_assum SUBST_ALL_TAC
-    \\ pop_assum SUBST_ALL_TAC
-    \\ `l < b ** n` by ( qunabbrev_tac`l` \\ qunabbrev_tac`n`
-                         \\ irule l2n_lt \\ simp[] )
-    \\ Cases_on`a = b - 1` \\ gs[] )
-  \\ strip_tac
-  \\ rewrite_tac[LEFT_SUB_DISTRIB]
-  \\ qpat_x_assum`_ = a`(SUBST1_TAC o SYM)
-  \\ gs[SUB_LEFT_ADD] \\ rw[]
-  \\ Cases_on`n=0` \\ gs[]
-  \\ `b ** n <= b ** 0` by simp[]
-  \\ gs[EXP_BASE_LE_IFF]
-QED
-
-Theorem l2n_2_neg:
-  !ls.
-  EVERY ($> 2) ls ==>
-  2 ** LENGTH ls - SUC (l2n 2 ls) = l2n 2 (MAP (\x. 1 - x) ls)
-Proof
-  Induct
-  \\ rw[l2n_def]
-  \\ gs[EXP, ADD1]
-  \\ first_x_assum(CHANGED_TAC o SUBST1_TAC o SYM)
-  \\ simp[LEFT_SUB_DISTRIB, LEFT_ADD_DISTRIB, SUB_RIGHT_ADD]
-  \\ qspecl_then[`ls`,`2`]mp_tac l2n_lt
-  \\ simp[]
-QED
-
-Theorem word_not_bits:
-  LENGTH ls = dimindex(:'a) /\ EVERY ($> 2) ls ==>
-  ¬word_from_bin_list ls : 'a word =
-  word_from_bin_list (MAP (λx. 1 - x) ls)
-Proof
-  rw[word_from_bin_list_def, l2w_def]
-  \\ rewrite_tac[word_2comp_n2w]
-  \\ Cases_on`l2n 2 ls = dimword(:'a) - 1`
-  >- (
-    mp_then Any (qspec_then`ls`mp_tac)
-      l2n_max (SIMP_CONV(srw_ss())[]``0 < 2n`` |> EQT_ELIM)
-    \\ `dimword (:'a) = 2 ** LENGTH ls` by simp[dimword_def]
-    \\ first_assum (SUBST_ALL_TAC o SYM)
-    \\ pop_assum kall_tac
-    \\ pop_assum SUBST_ALL_TAC
-    \\ simp[ADD1, ZERO_LT_dimword]
-    \\ strip_tac
-    \\ qmatch_goalsub_abbrev_tac`A MOD N = 0`
-    \\ `A = 0` suffices_by rw[]
-    \\ rw[Abbr`A`, l2n_eq_0]
-    \\ gs[EVERY_MAP, EVERY_MEM]
-    \\ rw[]
-    \\ `2 > x` by simp[]
-    \\ `x < 2` by simp[]
-    \\ pop_assum mp_tac
-    \\ `x MOD 2 = 1` by simp[]
-    \\ rewrite_tac[NUMERAL_LESS_THM]
-    \\ strip_tac \\ fs[] )
-  \\ `SUC (l2n 2 ls) < dimword(:'a)`
-  by (
-    qspecl_then[`ls`,`2`]mp_tac l2n_lt
-    \\ gs[dimword_def] )
-  \\ qmatch_goalsub_abbrev_tac`_ = n2w $ l2n 2 l1`
-  \\ `l2n 2 l1 < dimword(:'a)`
-  by (
-    qspecl_then[`l1`,`2`]mp_tac l2n_lt
-    \\ gs[dimword_def, Abbr`l1`] )
-  \\ simp[Abbr`l1`]
-  \\ drule l2n_2_neg
-  \\ simp[dimword_def]
-QED
-
 Theorem concat_word_list_bytes_to_64:
   LENGTH (ls: word8 list) = 8 ⇒
   concat_word_list ls : word64 =
@@ -672,6 +70,43 @@ Proof
   \\ simp[]
 QED
 
+Theorem cv_LEN_add:
+  cv_LEN cv (Num n) =
+  cv_add (Num n) (cv_LEN cv (Num 0))
+Proof
+  qid_spec_tac`n`
+  \\ Induct_on`cv`
+  >- ( rw[Once cv_LEN_def] \\ rw[Once cv_LEN_def] )
+  \\ rewrite_tac[Once cv_LEN_def]
+  \\ simp_tac (srw_ss()) []
+  \\ gen_tac
+  \\ simp_tac std_ss [Once cv_LEN_def, SimpRHS]
+  \\ simp_tac (srw_ss()) []
+  \\ first_assum(qspec_then`n + 1`SUBST1_TAC)
+  \\ first_assum(qspec_then`1`SUBST1_TAC)
+  \\ qmatch_goalsub_abbrev_tac`cv_add _ p`
+  \\ Cases_on`p`
+  \\ simp[]
+QED
+
+Theorem DIV2_SBIT:
+  DIV2 (SBIT b n) = if n = 0 then 0 else SBIT b (n - 1)
+Proof
+  qspecl_then[`b`,`n`,`1`]mp_tac SBIT_DIV
+  \\ simp[DIV2_def]
+  \\ Cases_on`1 < n` \\ gs[]
+  \\ Cases_on`n=0` \\ gs[SBIT_def]
+  \\ rw[]
+  \\ `n=1` by gs[]
+  \\ gvs[]
+QED
+
+Theorem ODD_SBIT:
+  ODD (SBIT b n) = (b /\ n = 0)
+Proof
+  rw[SBIT_def, ODD_EXP_IFF]
+QED
+
 (*
 Theorem word_to_bytes_from_bin_list:
   word_to_bytes (word_from_bin_list ls :'a word) F =
@@ -3641,7 +3076,7 @@ Proof
   \\ conj_asm1_tac
   >- (
     DEP_REWRITE_TAC[LENGTH_chunks]
-    \\ simp[NULL_LENGTH]
+    \\ simp[NULL_GENLIST, MAP_GENLIST]
     \\ rw[Abbr`n`, divides_def, bool_to_bit_def] )
   \\ rpt strip_tac
   \\ DEP_REWRITE_TAC[EL_MAP]
@@ -3658,8 +3093,8 @@ Proof
     \\ disch_then drule \\ simp[] )
   \\ AP_TERM_TAC
   \\ DEP_REWRITE_TAC[EL_chunks]
-  \\ simp[NULL_LENGTH]
-  \\ conj_asm1_tac >- ( rw[Abbr`n`] \\ strip_tac \\ gs[] )
+  \\ simp[NULL_GENLIST, MAP_GENLIST]
+  \\ conj_asm1_tac >- ( rw[Abbr`n`, NULL_LENGTH] \\ strip_tac \\ gs[] )
   \\ simp[LIST_EQ_REWRITE, LENGTH_TAKE_EQ]
   \\ reverse IF_CASES_TAC
   >- ( pop_assum mp_tac \\ simp[Abbr`n`] )
@@ -3710,7 +3145,7 @@ Proof
   \\ conj_asm1_tac
   >- (
     DEP_REWRITE_TAC[LENGTH_chunks]
-    \\ simp[NULL_LENGTH]
+    \\ simp[MAP_GENLIST, NULL_GENLIST]
     \\ simp[bool_to_bit_def, divides_def, Abbr`n`] )
   \\ rpt strip_tac
   \\ DEP_REWRITE_TAC[EL_MAP]
@@ -3729,7 +3164,8 @@ Proof
     \\ (reverse conj_tac >- simp[])
     \\ rewrite_tac[LT_ADD_LCANCEL]
     \\ simp[Abbr`y`] )
-  \\ DEP_REWRITE_TAC[word_not_bits, EL_chunks]
+  \\ DEP_REWRITE_TAC[word_from_bin_list_not, EL_chunks]
+  \\ simp[NULL_GENLIST, MAP_GENLIST]
   \\ simp[NULL_LENGTH]
   \\ conj_tac
   >- (
@@ -3808,7 +3244,7 @@ Proof
   \\ pop_assum mp_tac
   \\ CONV_TAC(LAND_CONV(SIMP_CONV std_ss [NUMERAL_LESS_THM]))
   \\ strip_tac \\ rpt BasicProvers.VAR_EQ_TAC
-  \\ simp_tac (srw_ss()) []
+  \\ simp_tac (srw_ss()) [bool_to_bit_def]
   \\ EVAL_TAC
 QED
 
@@ -4159,7 +3595,7 @@ Proof
     >- (
       DEP_REWRITE_TAC[LENGTH_chunks]
       \\ simp[NULL_LENGTH]
-      \\ EVAL_TAC )
+      \\ EVAL_TAC \\ rw[bool_to_bit_def] )
     \\ rw[EL_REPLICATE, EL_MAP]
     \\ DEP_REWRITE_TAC[EL_chunks]
     \\ simp[NULL_LENGTH]
@@ -4725,12 +4161,6 @@ Proof
   rewrite_tac [GSYM sptreeTheory.LENGTH_toSortedAList] \\ rw []
 QED
 
-Triviality GENLIST_EQ_NIL:
-  GENLIST f n = [] ⇔ n = 0
-Proof
-  Cases_on ‘n’ \\ gvs [GENLIST]
-QED
-
 Triviality size_while1_neq_0:
   ∀a tt ww x y w z s.
     size s ≠ 0 ⇒

From dbc44ca145114906790628d739b908c5edb4c300 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 18 Dec 2024 12:53:16 +0000
Subject: [PATCH 25/27] Add Keccak to selftest level 1

---
 src/parallel_builds/core/Holmakefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/parallel_builds/core/Holmakefile b/src/parallel_builds/core/Holmakefile
index 4ef8ca1c3f..8ac2d8d082 100644
--- a/src/parallel_builds/core/Holmakefile
+++ b/src/parallel_builds/core/Holmakefile
@@ -32,7 +32,7 @@ ifdef HOLSELFTESTLEVEL
 # example directories to build at selftest level 1
 EXDIRS = algebra/aat \
          arm/arm6-verification arm/armv8-memory-model arm/experimental \
-         CCS Crypto/RSA Crypto/SHA-2 Hoare-for-divergence MLsyntax \
+         CCS Crypto/RSA Crypto/SHA-2 Crypto/Keccak Hoare-for-divergence MLsyntax \
          PSL/1.01/executable-semantics PSL/1.1/official-semantics \
 	 STE algorithms computability countchars dependability dev \
          developers/ThmSetData \

From d5707e11d9289e609bff5ff8c6871d22cf914f84 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 18 Dec 2024 12:54:33 +0000
Subject: [PATCH 26/27] Comment out cheated theorem

---
 examples/Crypto/Keccak/keccakScript.sml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 2305a9bd51..10a85956ae 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -3683,6 +3683,7 @@ Definition Keccak_256_bytes_def:
     MAP (PAD_RIGHT 0 8 o word_to_bin_list) bs
 End
 
+(*
 Theorem Keccak_256_w64_thm:
   Keccak_256_w64 = Keccak_256_bytes
 Proof
@@ -3721,6 +3722,7 @@ Proof
   \\ simp[MAP_TAKE, GSYM chunks_MAP]
   \\ cheat
 QED
+*)
 
 (* TODO: move/replace *)
 Definition hex_to_rev_bytes_def:

From 30da3bd60bb1e79b0fd65bcf95c75bf58094b077 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 18 Dec 2024 13:06:37 +0000
Subject: [PATCH 27/27] Upstream another theorem about word_from_bin_list

---
 examples/Crypto/Keccak/keccakScript.sml | 60 +++----------------------
 src/n-bit/wordsScript.sml               | 48 ++++++++++++++++++++
 2 files changed, 55 insertions(+), 53 deletions(-)

diff --git a/examples/Crypto/Keccak/keccakScript.sml b/examples/Crypto/Keccak/keccakScript.sml
index 10a85956ae..598322f312 100644
--- a/examples/Crypto/Keccak/keccakScript.sml
+++ b/examples/Crypto/Keccak/keccakScript.sml
@@ -2470,52 +2470,6 @@ Proof
   \\ simp[] \\ strip_tac \\ simp[bool_to_bit_def]
 QED
 
-Theorem word_xor_bits_neq:
-  LENGTH b1 = LENGTH b2 ==>
-  word_from_bin_list b1 ?? word_from_bin_list b2 =
-  word_from_bin_list (MAP (λ(x,y). (x + y) MOD 2) (ZIP (b1, b2)))
-Proof
-  qid_spec_tac`b2`
-  \\ Induct_on`b1`
-  \\ rw[]
-  >- EVAL_TAC
-  \\ Cases_on`b2` \\ gs[]
-  \\ gs[word_from_bin_list_def, l2w_def, l2n_def]
-  \\ gs[GSYM word_add_n2w, GSYM word_mul_n2w]
-  \\ first_x_assum(qspec_then`t`(mp_tac o GSYM))
-  \\ simp[] \\ disch_then kall_tac
-  \\ DEP_REWRITE_TAC[WORD_ADD_XOR]
-  \\ `n2w 2 = n2w (2 ** 1)` by simp[]
-  \\ pop_assum SUBST_ALL_TAC
-  \\ simp[GSYM WORD_MUL_LSL]
-  \\ rewrite_tac[LSL_BITWISE]
-  \\ DEP_REWRITE_TAC[word_and_lsl_eq_0]
-  \\ simp[]
-  \\ conj_tac
-  >- (
-    rw[]
-    \\ Cases_on`2 < dimword(:'a)` \\ gs[MOD_LESS, MOD_MOD_LESS_EQ]
-    \\ Cases_on`dimword(:'a) = 2` \\ gs[MOD_MOD]
-    \\ `dimword(:'a) = 1` by simp[ZERO_LT_dimword]
-    \\ gs[] )
-  \\ rewrite_tac[GSYM WORD_XOR_ASSOC]
-  \\ AP_THM_TAC \\ AP_TERM_TAC
-  \\ AP_THM_TAC \\ AP_TERM_TAC
-  \\ qmatch_goalsub_rename_tac`x + y`
-  \\ `x MOD 2 < 2 ∧ y MOD 2 < 2` by simp[]
-  \\ ntac 2 (pop_assum mp_tac)
-  \\ rewrite_tac[NUMERAL_LESS_THM]
-  \\ Cases_on`ODD (x + y)`
-  >- (
-    `(x + y) MOD 2 = 1` by gs[ODD_MOD2_LEM]
-    \\ gs[ODD_ADD]
-    \\ Cases_on`ODD x` \\ gs[ODD_MOD2_LEM] )
-  \\ gs[GSYM EVEN_ODD]
-  \\ drule (iffLR EVEN_ADD)
-  \\ gs[EVEN_MOD2]
-  \\ Cases_on`x MOD 2 = 0` \\ gs[]
-QED
-
 Theorem xor_state_bools_w64:
   state_bools_w64 b1 w1 /\
   state_bools_w64 b2 w2
@@ -2545,7 +2499,7 @@ Proof
     \\ DEP_REWRITE_TAC[EL_chunks]
     \\ gs[NULL_EQ, bool_to_bit_def, divides_def]
     \\ rw[] \\ strip_tac \\ gs[] )
-  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ DEP_REWRITE_TAC[word_from_bin_list_xor]
   \\ simp[]
   \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 1 |> DISCH_ALL]
   \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 2 |> DISCH_ALL]
@@ -2603,7 +2557,7 @@ Proof
   \\ conj_tac >- ( rw[Abbr`n`] \\ strip_tac \\ gs[] )
   \\ conj_tac >- ( rw[Abbr`n`, divides_def] \\ strip_tac \\ gs[] )
   \\ simp[GSYM MAP_DROP, GSYM MAP_TAKE]
-  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ DEP_REWRITE_TAC[word_from_bin_list_xor]
   \\ conj_tac >- simp[Abbr`n`]
   \\ AP_TERM_TAC
   \\ DEP_REWRITE_TAC[ZIP_MAP |> SPEC_ALL |> UNDISCH |> cj 1 |> DISCH_ALL]
@@ -2669,7 +2623,7 @@ Proof
   \\ `MIN (n - 1) n = n - 1` by simp[Abbr`n`]
   \\ simp[LASTN_DROP, BUTLASTN_TAKE]
   \\ simp[GSYM MAP_DROP, GSYM MAP_TAKE, DROP_GENLIST, TAKE_GENLIST]
-  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ DEP_REWRITE_TAC[word_from_bin_list_xor]
   \\ conj_tac >- simp[Abbr`n`]
   \\ AP_TERM_TAC
   \\ rewrite_tac[GSYM MAP_APPEND, GSYM MAP]
@@ -2743,7 +2697,7 @@ Proof
     \\ DEP_REWRITE_TAC[LENGTH_chunks]
     \\ gs[NULL_EQ]
     \\ rpt strip_tac \\ gs[] )
-  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ DEP_REWRITE_TAC[word_from_bin_list_xor]
   \\ conj_tac >- simp[]
   \\ AP_TERM_TAC
   \\ rewrite_tac[GSYM MAP_DROP, GSYM MAP_TAKE]
@@ -3175,7 +3129,7 @@ Proof
     \\ rw[EVERY_MEM] \\ rw[] )
   \\ DEP_REWRITE_TAC[word_from_bin_list_and]
   \\ simp[]
-  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ DEP_REWRITE_TAC[word_from_bin_list_xor]
   \\ simp[]
   \\ AP_TERM_TAC
   \\ simp[LIST_EQ_REWRITE, LENGTH_TAKE_EQ]
@@ -3335,7 +3289,7 @@ Proof
   \\ `g = word_from_bin_list (PAD_RIGHT 0 64 $ word_to_bin_list g)`
   by simp[word_from_bin_list_def, word_to_bin_list_def, l2w_w2l]
   \\ pop_assum SUBST1_TAC
-  \\ DEP_REWRITE_TAC[word_xor_bits_neq]
+  \\ DEP_REWRITE_TAC[word_from_bin_list_xor]
   \\ simp[]
   \\ AP_TERM_TAC
   \\ BasicProvers.VAR_EQ_TAC
@@ -3650,7 +3604,7 @@ Proof
       \\ simp[NULL_LENGTH]
       \\ conj_tac >- (rpt strip_tac \\ gs[MAP2_MAP, ZIP_EQ_NIL])
       \\ conj_tac >- (rpt strip_tac \\ gs[MAP2_MAP, ZIP_EQ_NIL])
-      \\ simp[word_xor_bits_neq]
+      \\ simp[word_from_bin_list_xor]
       \\ AP_TERM_TAC
       \\ simp[LIST_EQ_REWRITE]
       \\ rpt strip_tac
diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml
index 0d2a7c4223..2389480103 100644
--- a/src/n-bit/wordsScript.sml
+++ b/src/n-bit/wordsScript.sml
@@ -5230,6 +5230,54 @@ Proof
   \\ simp[dimword_def]
 QED
 
+Theorem word_from_bin_list_xor:
+  LENGTH b1 = LENGTH b2 ==>
+  word_from_bin_list b1 ?? word_from_bin_list b2 =
+  word_from_bin_list (MAP (\(x,y). (x + y) MOD 2) (ZIP (b1, b2)))
+Proof
+  qid_spec_tac`b2`
+  \\ Induct_on`b1`
+  \\ rw[]
+  >- (EVAL_TAC \\ rw[WORD_XOR_CLAUSES])
+  \\ Cases_on`b2` \\ gs[]
+  \\ gs[word_from_bin_list_def, l2w_def, l2n_def]
+  \\ gs[GSYM word_add_n2w, GSYM word_mul_n2w]
+  \\ first_x_assum(qspec_then`t`(mp_tac o GSYM))
+  \\ simp[] \\ disch_then kall_tac
+  \\ DEP_REWRITE_TAC[WORD_ADD_XOR]
+  \\ `n2w 2 = n2w (2 ** 1)` by simp[]
+  \\ pop_assum SUBST_ALL_TAC
+  \\ simp[GSYM WORD_MUL_LSL]
+  \\ rewrite_tac[LSL_BITWISE]
+  \\ DEP_REWRITE_TAC[word_and_lsl_eq_0]
+  \\ simp[]
+  \\ conj_tac
+  >- (
+    rw[]
+    \\ Cases_on`2 < dimword(:'a)` \\ gs[MOD_LESS, MOD_MOD_LESS_EQ]
+    \\ Cases_on`dimword(:'a) = 2` \\ gs[MOD_MOD]
+    \\ `dimword(:'a) = 1` by simp[ZERO_LT_dimword]
+    \\ gs[] )
+  \\ rewrite_tac[GSYM WORD_XOR_ASSOC, GSYM LSL_BITWISE]
+  \\ AP_THM_TAC \\ AP_TERM_TAC
+  \\ rewrite_tac[Once WORD_XOR_COMM]
+  \\ rewrite_tac[GSYM WORD_XOR_ASSOC]
+  \\ AP_THM_TAC \\ AP_TERM_TAC
+  \\ qmatch_goalsub_rename_tac`x + y`
+  \\ `x MOD 2 < 2 /\ y MOD 2 < 2` by simp[]
+  \\ ntac 2 (pop_assum mp_tac)
+  \\ rewrite_tac[NUMERAL_LESS_THM]
+  \\ Cases_on`ODD (x + y)`
+  >- (
+    `(x + y) MOD 2 = 1` by gs[ODD_MOD2_LEM]
+    \\ gs[ODD_ADD]
+    \\ Cases_on`ODD x` \\ gs[ODD_MOD2_LEM, WORD_XOR_CLAUSES] )
+  \\ gs[GSYM EVEN_ODD]
+  \\ drule (iffLR EVEN_ADD)
+  \\ gs[EVEN_MOD2]
+  \\ Cases_on`x MOD 2 = 0` \\ gs[WORD_XOR_CLAUSES]
+QED
+
 (* -------------------------------------------------------------------------
     Create a few word sizes
    ------------------------------------------------------------------------- *)