diff --git a/misc/byteScript.sml b/misc/byteScript.sml index 7e58e97217..2745b24d5c 100644 --- a/misc/byteScript.sml +++ b/misc/byteScript.sml @@ -298,4 +298,537 @@ Proof \\ simp[] QED +Definition word_to_bytes_aux_def: (* length, 'a word, endianness *) + word_to_bytes_aux 0 (w:'a word) be = [] ∧ + word_to_bytes_aux (SUC n) w be = + (word_to_bytes_aux n w be) ++ [get_byte (n2w n) w be] +End +(* cyclic repeat as get_byte does when length > bytes_in_word for 'a*) + +Definition word_to_bytes_def: + word_to_bytes (w:'a word) be = + word_to_bytes_aux (dimindex (:'a) DIV 8) w be +End + +Theorem byte_index_cycle: + 8 ≤ dimindex (:'a) ⇒ + byte_index (n2w ((w2n (a:'a word)) MOD (dimindex (:'a) DIV 8)):'a word) be = byte_index a be +Proof + strip_tac>> + simp[byte_index_def]>> + ‘0 < dimindex(:'a) DIV 8’ + by (CCONTR_TAC>>fs[NOT_LESS]>> + fs[DIV_EQ_0])>> + ‘w2n a MOD (dimindex (:'a) DIV 8) < dimword (:'a)’ + by (irule LESS_EQ_LESS_TRANS>> + irule_at Any w2n_lt>> + irule_at Any MOD_LESS_EQ>>fs[])>> + simp[MOD_MOD] +QED + +Theorem get_byte_cycle: + 8 ≤ dimindex (:'a) ⇒ + get_byte (n2w ((w2n (a:'a word)) MOD (dimindex (:'a) DIV 8)):'a word) w be + = get_byte a w be +Proof + rw[get_byte_def,byte_index_cycle] +QED + +Theorem set_byte_cycle: + 8 ≤ dimindex (:'a) ⇒ + set_byte (n2w ((w2n (a:'a word)) MOD (dimindex (:'a) DIV 8)):'a word) b w be + = set_byte a b w be +Proof + rw[set_byte_def,byte_index_cycle] +QED + +Theorem word_slice_alt_word_slice: + h ≤ dimindex (:'a) ⇒ + word_slice_alt (SUC h) l w = word_slice h l (w:'a word) +Proof + rw[word_slice_alt_def,word_slice_def]>> + simp[GSYM WORD_EQ]>>rpt strip_tac>> + srw_tac[wordsLib.WORD_BIT_EQ_ss][]>> + simp[EQ_IMP_THM]>>rw[] +QED + +Theorem word_slice_shift: + h < dimindex (:'a) ⇒ + word_slice h l (w:'a word) = w ⋙ l ≪ l ≪ (dimindex (:'a) - (SUC h)) ⋙ (dimindex (:'a) - (SUC h)) +Proof + strip_tac>> + Cases_on ‘l ≤ h’>>fs[NOT_LESS_EQUAL,WORD_SLICE_ZERO]>> + simp[WORD_SLICE_THM]>> + simp[word_lsr_n2w,ADD1]>> + simp[WORD_BITS_LSL]>> + simp[WORD_BITS_COMP_THM]>> + simp[MIN_DEF]>> + rewrite_tac[SUB_RIGHT_ADD]>> + IF_CASES_TAC>>fs[] +QED + +Theorem word_slice_alt_shift: + h ≤ dimindex (:'a) ⇒ + word_slice_alt h l (w:'a word) = w ⋙ l ≪ l ≪ (dimindex (:'a) - h) ⋙ (dimindex (:'a) - h) +Proof + strip_tac>> + Cases_on ‘h’>>fs[]>- + srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def]>> + rw[word_slice_alt_word_slice,word_slice_shift] +QED + +Theorem byte_index_offset: + 8 ≤ dimindex (:'a) ⇒ + byte_index (a:'a word) be + 8 ≤ dimindex (:'a) +Proof + strip_tac>> + ‘0 < dimindex (:'a) DIV 8’ by + (simp[GSYM NOT_ZERO_LT_ZERO]>> + strip_tac>> + ‘dimindex (:'a) < 8’ by + (irule DIV_0_IMP_LT>>simp[])>>simp[])>> + assume_tac (Q.SPECL [‘dimindex(:'a)’,‘8’] DA)>> + fs[]>> + rw[byte_index_def]>- + (simp[LEFT_SUB_DISTRIB]>> + simp[LEFT_ADD_DISTRIB]>> + rewrite_tac[SUB_PLUS]>> + irule LESS_EQ_TRANS>> + qexists_tac ‘8 * (dimindex (:'a) DIV 8)’>> + simp[]>> + qpat_x_assum ‘_ = dimindex (:'a)’ $ assume_tac o GSYM>> + first_assum (fn h => rewrite_tac[h])>> + fs[GSYM DIV_EQ_0])>> + irule LESS_EQ_TRANS>> + qexists_tac ‘8 * ((w2n a MOD (dimindex (:'a) DIV 8)) + 1)’>> + conj_tac >- simp[LEFT_ADD_DISTRIB]>> + irule LESS_EQ_TRANS>> + irule_at Any (iffRL LE_MULT_LCANCEL)>> + simp[GSYM ADD1]>>simp[GSYM LESS_EQ]>> + irule_at Any MOD_LESS>> + simp[]>> + qpat_x_assum ‘_ = dimindex (:'a)’ $ assume_tac o GSYM>> + first_assum (fn h => rewrite_tac[h])>> + simp[]>> + fs[GSYM DIV_EQ_0] +QED + +Theorem DIV_not_0: + 1 < d ⇒ (d ≤ n ⇔ 0 < n DIV d) +Proof + strip_tac>> + drule DIV_EQ_0>>strip_tac>> + first_x_assum $ qspec_then ‘n’ assume_tac>>fs[] +QED + +Theorem get_byte_set_byte_irrelevant: + 16 ≤ dimindex (:'a) ∧ + w2n (a:α word) MOD (dimindex(:α) DIV 8) ≠ w2n a' MOD (dimindex(:α) DIV 8) ⇒ + get_byte a' (set_byte a b w be) be = get_byte a' w be +Proof + strip_tac>> + rewrite_tac[set_byte_def,get_byte_def]>> + simp[GSYM WORD_w2w_OVER_BITWISE]>> + ‘0 < dimindex (:'a) DIV 8’ + by (simp[GSYM NOT_ZERO_LT_ZERO]>> + strip_tac>> + ‘dimindex (:'a) < 8’ + by (irule DIV_0_IMP_LT>>simp[])>>simp[])>> + ‘w2n a' MOD (dimindex (:α) DIV 8) < dimindex (:α) DIV 8’ by + simp[MOD_LESS]>> + ‘w2n a MOD (dimindex (:α) DIV 8) < dimindex (:α) DIV 8’ by + simp[MOD_LESS]>> + ‘byte_index a be + 8 ≤ dimindex (:'a)’ by fs[byte_index_offset]>> + ‘byte_index a' be + 8 ≤ dimindex (:'a)’ by fs[byte_index_offset]>> + simp[word_slice_alt_shift]>> + simp[w2w_def,w2n_lsr]>> + simp[WORD_MUL_LSL]>> + simp[word_mul_n2w]>> + simp[word_mul_def]>> + ‘(w2n (w ⋙ (byte_index a be + 8)) * 2 ** (byte_index a be + 8)) < dimword (:α)’ by + (simp[w2n_lsr]>> + ‘0:num < 2 ** (byte_index a be + 8)’ by simp[]>> + drule DA>>disch_then $ qspec_then ‘w2n w’ mp_tac>>strip_tac>> + simp[]>>rewrite_tac[Once ADD_COMM]>>simp[DIV_MULT]>> + irule LESS_EQ_LESS_TRANS>> + irule_at Any w2n_lt>> + qexists_tac ‘w’>>simp[])>> + ‘(w2n b * 2 ** byte_index a be) < dimword (:α)’ by + (irule LESS_LESS_EQ_TRANS>> + irule_at Any (iffRL LT_MULT_RCANCEL)>> + irule_at Any w2n_lt>> + simp[dimword_def]>> + irule LESS_EQ_TRANS>> + irule_at Any (iffRL EXP_BASE_LE_MONO)>> + qexists_tac ‘byte_index a be + 8’>>simp[EXP_ADD])>> + simp[MOD_LESS]>> + qmatch_goalsub_abbrev_tac ‘w1 ‖ w2 ‖ w3’>> + qpat_x_assum ‘_ ≠ _’ mp_tac>> + simp[NOT_NUM_EQ,GSYM LESS_EQ]>>strip_tac>- + (‘if be then byte_index a' be < byte_index a be + else byte_index a be < byte_index a' be’ by rw[byte_index_def]>> + Cases_on ‘be’>>simp[]>- + (‘w1 = 0w ∧ w3 = n2w (w2n w DIV 2 ** byte_index a' T) ∧ w2 = 0w’ by + (conj_tac >- + (simp[Abbr ‘w1’]>> + simp[w2n_lsr]>> + ‘0:num < 2 ** (byte_index a T + 8)’ by simp[ZERO_LT_EXP]>> + drule DA>>disch_then $ qspec_then ‘w2n w’ mp_tac>>strip_tac>> + simp[]>> + rewrite_tac[Once ADD_COMM]>> + simp[DIV_MULT]>> + simp[EXP_ADD]>> + qpat_x_assum ‘if _ then _ else _’ mp_tac>> + simp[LESS_EQ,ADD1]>>strip_tac>> + drule LESS_EQUAL_ADD>>strip_tac>> + simp[EXP_ADD]>> + ntac 2 (rewrite_tac[Once MULT_ASSOC])>> + simp[MULT_DIV])>> + ‘byte_index a' T + 8 ≤ byte_index a T’ by + (simp[byte_index_def]>> + irule LESS_EQ_TRANS>> + qexists_tac ‘8 * (dimindex (:α) DIV 8 − (w2n a' MOD (dimindex (:α) DIV 8) + 1) + 1)’>> + simp[]>> + rewrite_tac[Once $ GSYM ADD1]>> + simp[GSYM LESS_EQ]>> + ‘w2n a' MOD (dimindex (:α) DIV 8) < dimindex (:α) DIV 8’ by + simp[MOD_LESS]>> + simp[])>> + conj_tac >- + (simp[Abbr ‘w3’]>> + ‘dimword (:'a) = + 2 ** (dimindex (:α) + byte_index a' T − byte_index a T) + * 2 ** (byte_index a T - byte_index a' T)’ by + fs[dimword_def,GSYM EXP_ADD]>> + pop_assum (fn h => rewrite_tac[h])>> + ‘0 < 2 ** (byte_index a T - byte_index a' T) ∧ + 0 < 2 ** (dimindex (:α) + byte_index a' T − byte_index a T)’ by + fs[ZERO_LT_EXP]>> + drule (GSYM DIV_MOD_MOD_DIV)>> + pop_assum kall_tac>> + disch_then $ drule>>strip_tac>> + pop_assum (fn h => rewrite_tac[h])>> + qmatch_goalsub_abbrev_tac ‘(_ * X) DIV Y’>> + ‘Y = X * 2 ** byte_index a' T’ by simp[Abbr ‘X’,Abbr ‘Y’,GSYM EXP_ADD]>> + pop_assum (fn h => rewrite_tac[h])>> + ‘0 < X ∧ 0 < 2 ** byte_index a' T’ by simp[ZERO_LT_EXP,Abbr ‘X’]>> + simp[GSYM DIV_DIV_DIV_MULT]>> + simp[Abbr ‘X’]>> + drule LESS_EQUAL_ADD>>strip_tac>> + simp[EXP_ADD]>> + simp[MOD_MULT_MOD,MULT_DIV])>> + simp[Abbr ‘w2’]>> + drule LESS_EQUAL_ADD>>strip_tac>> + simp[EXP_ADD,MULT_DIV]>> + rewrite_tac[Once MULT_ASSOC]>> + simp[MULT_DIV])>>simp[])>> + ‘byte_index a F + 8 ≤ byte_index a' F’ by simp[byte_index_def]>> + ‘w3 = 0w ∧ w1 = n2w (w2n w DIV 2 ** byte_index a' F) ∧ w2 = 0w’ by + (conj_tac >- + (simp[Abbr ‘w3’]>> + qmatch_goalsub_abbrev_tac ‘(_ * X) MOD _ DIV Y’>> + ‘Y = X * 2 ** byte_index a' F’ by simp[Abbr ‘Y’,Abbr ‘X’,GSYM EXP_ADD]>> + pop_assum (fn h => rewrite_tac[h])>> + simp[GSYM DIV_DIV_DIV_MULT,ZERO_LT_EXP,Abbr ‘X’]>> + ‘dimword (:'a) = + 2 ** (dimindex (:α) − byte_index a F) * 2 ** (byte_index a F)’ by + fs[dimword_def,GSYM EXP_ADD]>> + pop_assum (fn h => rewrite_tac[h])>> + simp[GSYM DIV_MOD_MOD_DIV,ZERO_LT_EXP,MULT_DIV]>> + qmatch_goalsub_abbrev_tac ‘X MOD _’>> + ‘w2n w MOD 2 ** byte_index a F < 2 ** byte_index a' F’ by + (irule LESS_TRANS>> + irule_at (Pos hd) MOD_LESS>> + simp[])>> + pop_assum mp_tac>> + DEP_ONCE_REWRITE_TAC[GSYM DIV_EQ_0]>> + simp[EXP])>> + conj_tac >- + (simp[Abbr ‘w1’]>> + simp[w2n_lsr]>> + ‘0 < 2 ** (byte_index a F + 8)’ by simp[]>> + drule DA>>disch_then $ qspec_then ‘w2n w’ mp_tac>> + strip_tac>> + simp[]>> + rewrite_tac[Once ADD_COMM]>> + simp[DIV_MULT]>> + drule LESS_EQUAL_ADD>>strip_tac>> + simp[]>> + qabbrev_tac ‘X = byte_index a F + 8’>> + simp[EXP_ADD]>> + simp[GSYM DIV_DIV_DIV_MULT]>> + rewrite_tac[Once ADD_COMM]>> + simp[DIV_MULT,MULT_DIV])>> + simp[Abbr ‘w2’]>> + drule LESS_EQUAL_ADD>>strip_tac>> + simp[]>> + simp[EXP_ADD]>> + rewrite_tac[MULT_ASSOC]>> + once_rewrite_tac[MULT_COMM]>> + simp[GSYM DIV_DIV_DIV_MULT,MULT_DIV]>> + ‘w2n b DIV 256 = 0’ by + (simp[DIV_EQ_0]>> + irule LESS_LESS_EQ_TRANS>> + irule_at Any w2n_lt>> + simp[])>> + simp[])>>simp[])>> + ‘if be then byte_index a be < byte_index a' be + else byte_index a' be < byte_index a be’ by rw[byte_index_def]>> + Cases_on ‘be’>>simp[]>- + (‘byte_index a T + 8 ≤ byte_index a' T’ by simp[byte_index_def]>> + ‘w3 = 0w ∧ w1 = n2w (w2n w DIV 2 ** byte_index a' T) ∧ w2 = 0w’ by + (conj_tac >- + (simp[Abbr ‘w3’]>> + qmatch_goalsub_abbrev_tac ‘(_ * X) MOD _ DIV Y’>> + ‘Y = X * 2 ** byte_index a' T’ by simp[Abbr ‘Y’,Abbr ‘X’,GSYM EXP_ADD]>> + pop_assum (fn h => rewrite_tac[h])>> + simp[GSYM DIV_DIV_DIV_MULT,ZERO_LT_EXP,Abbr ‘X’]>> + ‘dimword (:'a) = + 2 ** (dimindex (:α) − byte_index a T) * 2 ** (byte_index a T)’ by + fs[dimword_def,GSYM EXP_ADD]>> + pop_assum (fn h => rewrite_tac[h])>> + simp[GSYM DIV_MOD_MOD_DIV,ZERO_LT_EXP,MULT_DIV]>> + qmatch_goalsub_abbrev_tac ‘X MOD _’>> + ‘w2n w MOD 2 ** byte_index a T < 2 ** byte_index a' T’ by + (irule LESS_TRANS>> + irule_at (Pos hd) MOD_LESS>> + simp[])>> + pop_assum mp_tac>> + DEP_ONCE_REWRITE_TAC[GSYM DIV_EQ_0]>> + simp[EXP])>> + conj_tac >- + (simp[Abbr ‘w1’]>> + simp[w2n_lsr]>> + ‘0 < 2 ** (byte_index a T + 8)’ by simp[]>> + drule DA>>disch_then $ qspec_then ‘w2n w’ mp_tac>> + strip_tac>> + simp[]>> + rewrite_tac[Once ADD_COMM]>> + simp[DIV_MULT]>> + drule LESS_EQUAL_ADD>>strip_tac>> + simp[]>> + qabbrev_tac ‘X = byte_index a T + 8’>> + simp[EXP_ADD]>> + simp[GSYM DIV_DIV_DIV_MULT,MULT_DIV]>> + rewrite_tac[Once ADD_COMM]>> + simp[DIV_MULT])>> + simp[Abbr ‘w2’]>> + drule LESS_EQUAL_ADD>>strip_tac>> + simp[]>> + simp[EXP_ADD]>> + rewrite_tac[MULT_ASSOC]>> + once_rewrite_tac[MULT_COMM]>> + simp[GSYM DIV_DIV_DIV_MULT,MULT_DIV]>> + ‘w2n b DIV 256 = 0’ by + (simp[DIV_EQ_0]>> + irule LESS_LESS_EQ_TRANS>> + irule_at Any w2n_lt>> + simp[])>> + simp[])>>simp[])>> + ‘w1 = 0w ∧ w3 = n2w (w2n w DIV 2 ** byte_index a' F) ∧ w2 = 0w’ by + (conj_tac >- + (simp[Abbr ‘w1’]>> + simp[w2n_lsr]>> + ‘0 < 2 ** (byte_index a F + 8)’ by simp[ZERO_LT_EXP]>> + drule DA>>disch_then $ qspec_then ‘w2n w’ mp_tac>>strip_tac>> + simp[]>> + rewrite_tac[Once ADD_COMM]>> + simp[DIV_MULT]>> + simp[EXP_ADD]>> + qpat_x_assum ‘if _ then _ else _’ mp_tac>> + simp[LESS_EQ,ADD1]>>strip_tac>> + drule LESS_EQUAL_ADD>>strip_tac>> + simp[EXP_ADD]>> + ntac 2 (rewrite_tac[Once MULT_ASSOC])>> + simp[MULT_DIV])>> + ‘byte_index a' F + 8 ≤ byte_index a F’ by + (simp[byte_index_def]>> + irule LESS_EQ_TRANS>> + qexists_tac ‘8 * (dimindex (:α) DIV 8 − (w2n a' MOD (dimindex (:α) DIV 8) + 1) + 1)’>> + simp[]>> + rewrite_tac[Once $ GSYM ADD1]>> + simp[GSYM LESS_EQ]>> + ‘w2n a' MOD (dimindex (:α) DIV 8) < dimindex (:α) DIV 8’ by + simp[MOD_LESS]>> + simp[])>> + conj_tac >- + (simp[Abbr ‘w3’]>> + ‘dimword (:'a) = + 2 ** (dimindex (:α) + byte_index a' F − byte_index a F) + * 2 ** (byte_index a F - byte_index a' F)’ by + fs[dimword_def,GSYM EXP_ADD]>> + pop_assum (fn h => rewrite_tac[h])>> + ‘0 < 2 ** (byte_index a F - byte_index a' F) ∧ + 0 < 2 ** (dimindex (:α) + byte_index a' F − byte_index a F)’ by + fs[ZERO_LT_EXP]>> + simp[GSYM DIV_MOD_MOD_DIV]>> + qmatch_goalsub_abbrev_tac ‘(_ * X) DIV Y’>> + ‘Y = X * 2 ** byte_index a' F’ by simp[Abbr ‘X’,Abbr ‘Y’,GSYM EXP_ADD]>> + pop_assum (fn h => rewrite_tac[h])>> + ‘0 < X ∧ 0 < 2 ** byte_index a' F’ by simp[ZERO_LT_EXP,Abbr ‘X’]>> + simp[GSYM DIV_DIV_DIV_MULT]>> + drule LESS_EQUAL_ADD>>strip_tac>> + simp[EXP_ADD]>> + rewrite_tac[Once MULT_COMM]>> + simp[MOD_MULT_MOD,MULT_DIV])>> + simp[Abbr ‘w2’]>> + drule LESS_EQUAL_ADD>>strip_tac>> + simp[EXP_ADD]>> + rewrite_tac[Once MULT_ASSOC]>> + simp[MULT_DIV])>>simp[] +QED + +Theorem word_to_bytes_word_of_bytes_32: + LENGTH bs = dimindex (:32) DIV 8 ⇒ + word_to_bytes (word_of_bytes be (0w:word32) bs) be = bs +Proof + simp[word_to_bytes_def]>> + rewrite_tac[numLib.num_CONV “4”,numLib.num_CONV “3”,TWO,ONE, + word_to_bytes_aux_def]>> + simp[]>> + Cases_on ‘bs’>>simp[]>> + rename1 ‘_ ⇒ _ ∧ _ = bs’>>Cases_on ‘bs’>>simp[]>> + ntac 2 (SIMP_TAC std_ss [Once CONJ_ASSOC]>> + rename1 ‘_ ∧ _ = bs’>>Cases_on ‘bs’>>simp[])>> + rewrite_tac[numLib.num_CONV “4”,numLib.num_CONV “3”,TWO,ONE]>> + fs[]>>strip_tac>> + simp[word_of_bytes_def,get_byte_set_byte_irrelevant,get_byte_set_byte] +QED + +Theorem word_to_bytes_word_of_bytes_64: + LENGTH bs = dimindex (:64) DIV 8 ⇒ + word_to_bytes (word_of_bytes be (0w:word64) bs) be = bs +Proof + simp[word_to_bytes_def]>> + rewrite_tac[numLib.num_CONV “8”,numLib.num_CONV “7”,numLib.num_CONV “6”, + numLib.num_CONV “5”,numLib.num_CONV “4”,numLib.num_CONV “3”, + TWO,ONE,word_to_bytes_aux_def]>> + simp[]>> + Cases_on ‘bs’>>simp[]>> + rename1 ‘_ ∧ _ = bs’>>Cases_on ‘bs’>>simp[]>> + ntac 6 (SIMP_TAC std_ss [Once CONJ_ASSOC]>> + rename1 ‘_ ∧ _ = bs’>>Cases_on ‘bs’>>simp[])>> + rewrite_tac[numLib.num_CONV “8”,numLib.num_CONV “7”,numLib.num_CONV “6”, + numLib.num_CONV “5”,numLib.num_CONV “4”,numLib.num_CONV “3”, + TWO,ONE]>> + fs[]>>strip_tac>> + simp[word_of_bytes_def,get_byte_set_byte_irrelevant,get_byte_set_byte] +QED + +Theorem set_byte_get_byte: + 8 ≤ dimindex (:'a) ⇒ + set_byte a (get_byte (a:'a word) (w:'a word) be) w be = w +Proof + strip_tac>> + simp[get_byte_def,set_byte_def]>> + imp_res_tac byte_index_offset>> + first_x_assum $ qspecl_then [‘be’, ‘a’] assume_tac>> + qmatch_goalsub_abbrev_tac ‘w0 ‖ _ ‖ _’>> + ‘w0 = word_slice_alt (byte_index a be + 8) (byte_index a be) w’ by + (simp[Abbr ‘w0’]>> + ‘byte_index a be + 8 = SUC (byte_index a be + 7)’ by simp[]>> + simp[word_slice_alt_word_slice]>> + simp[WORD_SLICE_THM]>> + qmatch_goalsub_abbrev_tac ‘A ≪ _ = B ≪ _’>> + ‘A = B’ by + (simp[Abbr ‘A’,Abbr ‘B’]>> + simp[w2w_w2w,word_lsr_n2w]>> + simp[WORD_BITS_COMP_THM]>> + simp[MIN_DEF])>> + simp[])>>simp[]>> + srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def]>> + Cases_on ‘i < byte_index a be’>>fs[NOT_LESS]>> + Cases_on ‘i < byte_index a be + 8’>>fs[] +QED + +Theorem set_byte_get_byte_copy: + 8 ≤ dimindex (:'a) ⇒ + set_byte a (get_byte (a:'a word) (w:'a word) be) w' be = + word_slice (byte_index a be + 7) (byte_index a be) w ‖ + (if byte_index a be + 8 = dimindex (:'a) then 0w + else word_slice (dimindex (:α) - 1) (byte_index a be + 8) w') ‖ + if byte_index a be = 0 then 0w else word_slice (byte_index a be - 1) 0 w' +Proof + strip_tac>> + simp[get_byte_def,set_byte_def]>> + imp_res_tac byte_index_offset>> + first_x_assum $ qspecl_then [‘be’, ‘a’] assume_tac>> + qmatch_goalsub_abbrev_tac ‘w0 ‖ _ ‖ _’>> + ‘w0 = word_slice (byte_index a be + 7) (byte_index a be) w’ by + (simp[Abbr ‘w0’]>> + simp[WORD_SLICE_THM]>> + qmatch_goalsub_abbrev_tac ‘A ≪ _ = B ≪ _’>> + ‘A = B’ by + (simp[Abbr ‘A’,Abbr ‘B’]>> + simp[w2w_w2w,word_lsr_n2w]>> + simp[WORD_BITS_COMP_THM]>> + simp[MIN_DEF])>> + simp[])>>simp[]>> + Cases_on ‘byte_index a be’>>fs[]>> + Cases_on ‘byte_index a be + 8 = dimindex (:'a)’>>fs[]>> + srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def]>> + Cases_on ‘i ≤ n’>>fs[NOT_LESS] +QED + +Theorem set_byte_get_byte': + 8 ≤ dimindex (:'a) ⇒ + set_byte a (get_byte (a:'a word) (w:'a word) be) w be = w +Proof + rw[set_byte_get_byte_copy]>- + srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def]>- + (simp[WORD_SLICE_COMP_THM]>> + srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def])>- + (rewrite_tac[Once WORD_OR_COMM]>> + simp[WORD_SLICE_COMP_THM]>> + srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def])>> + qmatch_goalsub_abbrev_tac ‘w2 ‖ w3 ‖ w1’>> + ‘w3 ‖ w2 ‖ w1 = w’ by + (simp[Abbr ‘w2’]>> + simp[Abbr ‘w1’]>> + simp[WORD_SLICE_COMP_THM]>> + simp[Abbr ‘w3’]>> + rewrite_tac[Once WORD_OR_COMM]>> + drule byte_index_offset>> + disch_then $ qspecl_then [‘be’, ‘a’] assume_tac>> + simp[WORD_SLICE_COMP_THM]>> + srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def])>> + fs[] +QED + +Theorem word_slice_alt_zero: + word_slice_alt h l 0w = 0w +Proof + srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def] +QED + +Theorem word_to_bytes_word_of_bytes_32: + word_of_bytes be (0w:word32) (word_to_bytes (w:word32) be) = w +Proof + ‘8 ≤ dimindex (:32)’ by simp[]>> + simp[word_to_bytes_def]>> + rewrite_tac[numLib.num_CONV “4”,numLib.num_CONV “3”,TWO,ONE, + word_to_bytes_aux_def]>> + simp[]>> + simp[word_of_bytes_def]>> + simp[set_byte_get_byte_copy]>> + rpt (CASE_TAC>>fs[byte_index_def])>> + srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def] +QED + +Theorem word_to_bytes_word_of_bytes_64: + word_of_bytes be (0w:word64) (word_to_bytes (w:word64) be) = w +Proof + ‘8 ≤ dimindex (:64)’ by simp[]>> + simp[word_to_bytes_def]>> + rewrite_tac[numLib.num_CONV “8”,numLib.num_CONV “7”, + numLib.num_CONV “6”,numLib.num_CONV “5”, + numLib.num_CONV “4”,numLib.num_CONV “3”, + TWO,ONE,word_to_bytes_aux_def]>> + simp[]>> + simp[word_of_bytes_def]>> + simp[set_byte_get_byte_copy]>> + rpt (CASE_TAC>>fs[byte_index_def])>> + srw_tac[wordsLib.WORD_BIT_EQ_ss][word_slice_alt_def] +QED + val _ = export_theory();