# Theory WordOperations

```(*  Title:      RSAPSS/Wordoperations.thy
Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

section  ‹Extensions to the Word theory required for SHA1›

theory WordOperations
imports Word
begin

type_synonym bv = "bit list"

datatype HEX = x0 | x1 | x2 | x3 | x4 | x5 | x6 | x7 | x8 | x9 | xA | xB | xC | xD | xE | xF

definition
bvxor: "bvxor a b = bv_mapzip (⊕⇩b) a b"

definition
bvand: "bvand a b = bv_mapzip (∧⇩b) a b"

definition
bvor: "bvor a b = bv_mapzip (∨⇩b) a b"

primrec last where
"last [] = Zero"
| "last (x#r) = (if (r=[]) then x else (last r))"

primrec dellast where
"dellast [] = []"
| "dellast (x#r) = (if (r = []) then [] else (x#dellast r))"

fun bvrol where
"bvrol a 0 = a"
| "bvrol [] x = []"
| "bvrol (x#r) (Suc n) = bvrol (r@[x]) n"

fun bvror where
"bvror a 0 = a"
| "bvror [] x = []"
| "bvror x (Suc n) = bvror (last x # dellast x) n"

fun selecthelp where
"selecthelp [] n = (if (n <= 0) then [Zero] else (Zero # selecthelp [] (n-(1::nat))))"
| "selecthelp (x#l) n = (if (n <= 0) then [x] else (x # selecthelp l (n-(1::nat))))"

fun select where
"select [] i n = (if (i <= 0) then (selecthelp [] n) else select [] (i-(1::nat)) (n-(1::nat)))"
| "select (x#l) i n = (if (i <= 0) then (selecthelp (x#l) n) else select l (i-(1::nat)) (n-(1::nat)))"

definition
rev (select (rev (nat_to_bv ((bv_to_nat a) + (bv_to_nat b)))) 0 31)"

definition
bv_prepend: "bv_prepend x b bv = replicate x b @ bv"

primrec zerolist where
"zerolist 0 = []"
| "zerolist (Suc n) = zerolist n  @ [Zero]"

primrec hextobv where
"hextobv x0 = [Zero,Zero,Zero,Zero]"
| "hextobv x1 = [Zero,Zero,Zero,One]"
| "hextobv x2 = [Zero,Zero,One,Zero]"
| "hextobv x3 = [Zero,Zero,One,One]"
| "hextobv x4 = [Zero,One,Zero,Zero]"
| "hextobv x5 = [Zero,One,Zero,One]"
| "hextobv x6 = [Zero,One,One,Zero]"
| "hextobv x7 = [Zero,One,One,One]"
| "hextobv x8 = [One,Zero,Zero,Zero]"
| "hextobv x9 = [One,Zero,Zero,One]"
| "hextobv xA = [One,Zero,One,Zero]"
| "hextobv xB = [One,Zero,One,One]"
| "hextobv xC = [One,One,Zero,Zero]"
| "hextobv xD = [One,One,Zero,One]"
| "hextobv xE = [One,One,One,Zero]"
| "hextobv xF = [One,One,One,One]"

primrec hexvtobv where
"hexvtobv [] = []"
| "hexvtobv (x#r) = hextobv x @ hexvtobv r"

lemma selectlenhelp: "length (selecthelp l i) = (i + 1)"
proof (induct i arbitrary: l)
case 0
show "length (selecthelp l 0) = 0 + 1"
proof (cases l)
case Nil
then have "selecthelp l 0 = [Zero]" by simp
then show ?thesis by simp
next
case (Cons a as)
then have "selecthelp l 0 = [a]" by simp
then show ?thesis by simp
qed
next
case (Suc x)
show "length (selecthelp l (Suc x)) = (Suc x) + 1"
proof (cases l)
case Nil
then have "selecthelp l (Suc x) = Zero # selecthelp l x" by simp
then show "length (selecthelp l (Suc x)) = Suc x + 1" using Suc by simp
next
case (Cons a b)
then have "selecthelp l (Suc x) = a # selecthelp b x" by simp
then have "length (selecthelp l (Suc x)) = 1 + length (selecthelp b x)" by simp
then show "length (selecthelp l (Suc x)) = Suc x + 1" using Suc by simp
qed
qed

lemma selectlenhelp2:  "⋀i. ∀l j. ∃k. select l i j = select k 0 (j - i)"
proof (auto)
fix i
show "⋀l j. ∃k. select l i j = select k 0 (j - i)"
proof (induct i)
fix l and j
have "select l 0 j = select l 0 (j-(0::nat))" by simp
then show "∃k. select l 0 j = select k 0 (j - (0::nat))" by auto
next
case (Suc x)
have b: "select l (Suc x) j = select (tl l) x (j-(1::nat))"
proof (cases l)
case Nil
then have "select l (Suc x) j = select l x (j-(1::nat))" by simp
moreover have "tl l = l" using Nil by simp
ultimately show ?thesis by (simp)
next
then have "select l (Suc x) j = select tail x (j-(1::nat))" by simp
moreover have "tail = tl l" using Cons by simp
ultimately show ?thesis by simp
qed
have "∃k. select l x j = select k 0 (j - (x::nat))" using Suc by simp
moreover have  "∃k. select (tl l) x (j-(1::nat)) = select k 0 (j-(1::nat)-(x::nat))" using Suc[of "tl l" "j-(1::nat)"] by auto
ultimately have "∃k. select l (Suc x) j = select k 0 (j-(1::nat) - (x::nat))" using b by auto
then show "∃k. select l (Suc x) j = select k 0 (j - Suc x)" by simp
qed
qed

lemma selectlenhelp3: "∀j. select l 0 j = selecthelp l j"
proof
fix j
show "select l 0 j = selecthelp l j"
proof (cases l)
case Nil
assume "l=[]"
then show "select l 0 j = selecthelp l j" by simp
next
case (Cons a b)
then show "select l 0 j = selecthelp l j" by simp
qed
qed

lemma selectlen: "length (select l i j) = j - i + 1"
proof -
from selectlenhelp2 have "∃k. select l i j = select k 0 (j-i)" by simp
then have "∃k. length (select l i j) = length (select k 0 (j-i))" by auto
then have c: "∃k. length (select l i j) = length (selecthelp k (j-i))"
using selectlenhelp3 by simp
from c obtain k where d: "length (select l i j) = length (selecthelp k (j-i))" by auto
have "0<=j-i" by arith
then have "length (selecthelp k (j-i)) = j-i+1" using selectlenhelp by simp
then show "length (select l i j) = j-i+1" using d by simp
qed