From 632a1664bde19028d9f5b95ff2a3e87115fb17de Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Sun, 12 May 2019 10:13:46 +0100 Subject: [PATCH 1/3] Move some theorems to HOL --- misc/miscScript.sml | 81 --------------------------------------------- 1 file changed, 81 deletions(-) diff --git a/misc/miscScript.sml b/misc/miscScript.sml index fc3bd4145e..1cab3e5bf8 100644 --- a/misc/miscScript.sml +++ b/misc/miscScript.sml @@ -805,11 +805,6 @@ Theorem BIT_num_from_bin_list_leading qexists_tac`2 ** LENGTH l` >> simp[numposrepTheory.l2n_lt] ) -Theorem word_bit_test - `word_bit n w <=> ((w && n2w (2 ** n)) <> 0w:'a word)` - (srw_tac [wordsLib.WORD_BIT_EQ_ss, boolSimps.CONJ_ss] - [wordsTheory.word_index, DECIDE ``0n < d ==> (n <= d - 1) = (n < d)``]) - val least_from_def = Define` least_from P n = if (∃x. P x ∧ n ≤ x) then $LEAST (λx. P x ∧ n ≤ x) else $LEAST P` @@ -2956,44 +2951,6 @@ Theorem byte_align_extract \\ rw[alignmentTheory.align_def] \\ blastLib.BBLAST_TAC); -(* TODO - candidate for move to HOL *) -Theorem byte_align_aligned - `byte_aligned x ⇔ (byte_align x = x)` (EVAL_TAC); - -(* TODO - candidate for move to HOL *) -Theorem byte_aligned_add - `byte_aligned x ∧ byte_aligned y ⇒ byte_aligned (x+y)` - (rw[alignmentTheory.byte_aligned_def] - \\ metis_tac[alignmentTheory.aligned_add_sub_cor]); - -(* TODO - candidate for move to HOL *) -Theorem align_ls - `align p n <=+ n` - (simp[WORD_LS] - \\ Cases_on`n` - \\ fs[alignmentTheory.align_w2n] - \\ qmatch_asmsub_rename_tac`n < _` - \\ DEP_REWRITE_TAC[LESS_MOD] - \\ conj_asm2_tac >- fs[] - \\ DEP_REWRITE_TAC[GSYM X_LE_DIV] - \\ simp[]); - -(* TODO - candidate for move to HOL *) -Theorem align_lo - `¬aligned p n ⇒ align p n <+ n` - (simp[WORD_LO] - \\ Cases_on`n` - \\ fs[alignmentTheory.align_w2n, alignmentTheory.aligned_def] - \\ strip_tac - \\ qmatch_goalsub_abbrev_tac`a < b` - \\ `a ≤ b` suffices_by fs[] - \\ qmatch_asmsub_rename_tac`n < _` - \\ simp[Abbr`a`] - \\ DEP_REWRITE_TAC[LESS_MOD] - \\ conj_asm2_tac >- fs[] - \\ DEP_REWRITE_TAC[GSYM X_LE_DIV] - \\ simp[]); - Theorem aligned_between `¬aligned p n ∧ aligned p m ∧ align p n <+ m ⇒ n <+ m` (rw[WORD_LO] @@ -3279,44 +3236,6 @@ Theorem asm_write_bytearray_EL \\ simp[ADD1,GSYM word_add_n2w] \\ metis_tac[WORD_ADD_ASSOC,WORD_ADD_COMM]); -(* TODO - candidate for move to HOL *) -Theorem word_bit_thm - `!n w:'a word. word_bit n w <=> n < dimindex (:'a) /\ w ' n` - (fs [word_bit_def,LESS_EQ] \\ rw [] - \\ assume_tac DIMINDEX_GT_0 - \\ Cases_on `dimindex (:α)` \\ fs [LESS_EQ]); - -(* TODO - candidate for move to HOL *) -Theorem word_bit_and - `word_bit n (w1 && w2) <=> word_bit n w1 /\ word_bit n w2` - (fs [word_bit_def,word_and_def] \\ eq_tac \\ rw [] - \\ assume_tac DIMINDEX_GT_0 - \\ `n < dimindex (:'a)` by decide_tac - \\ fs [fcpTheory.FCP_BETA]); - -(* TODO - candidate for move to HOL *) -Theorem word_bit_or - `word_bit n (w1 || w2) <=> word_bit n w1 \/ word_bit n w2` - (fs [word_bit_def,word_or_def] \\ eq_tac \\ rw [] - \\ assume_tac DIMINDEX_GT_0 - \\ `n < dimindex (:'a)` by decide_tac - \\ fs [fcpTheory.FCP_BETA]); - -(* TODO - candidate for move to HOL *) -Theorem word_bit_lsl - `word_bit n (w << i) <=> - word_bit (n - i) (w:'a word) /\ n < dimindex (:'a) /\ i <= n` - (fs [word_bit_thm,word_lsl_def] \\ eq_tac \\ fs [] - \\ rw [] \\ rfs [fcpTheory.FCP_BETA]); - -(* TODO - candidate for move to HOL *) -Theorem word_msb_align - `p < dimindex(:'a) ⇒ (word_msb (align p w) = word_msb (w:'a word))` - (rw[alignmentTheory.align_bitwise_and,word_msb] - \\ rw[word_bit_and] - \\ rw[word_bit_lsl] - \\ rw[word_bit_test, MOD_EQ_0_DIVISOR, dimword_def]); - (* TODO: move to sptTheory *) val eq_shape_def = Define ` From 4ded65ad3479759c5274f28017b05ecf9300c189 Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Wed, 15 May 2019 04:51:13 +0100 Subject: [PATCH 2/3] Move more theorems to HOL --- misc/miscScript.sml | 72 --------------------------------------------- 1 file changed, 72 deletions(-) diff --git a/misc/miscScript.sml b/misc/miscScript.sml index 1cab3e5bf8..b0ac17c2b4 100644 --- a/misc/miscScript.sml +++ b/misc/miscScript.sml @@ -2951,29 +2951,6 @@ Theorem byte_align_extract \\ rw[alignmentTheory.align_def] \\ blastLib.BBLAST_TAC); -Theorem aligned_between - `¬aligned p n ∧ aligned p m ∧ align p n <+ m ⇒ n <+ m` - (rw[WORD_LO] - \\ fs[alignmentTheory.align_w2n, alignmentTheory.aligned_def] - \\ Cases_on`n` \\ Cases_on`m` \\ fs[] - \\ CCONTR_TAC \\ fs[NOT_LESS] - \\ qmatch_asmsub_abbrev_tac`n DIV d * d` - \\ `n DIV d * d <= n` by ( - DEP_REWRITE_TAC[GSYM X_LE_DIV] \\ fs[Abbr`d`] ) - \\ fs[] - \\ qmatch_asmsub_rename_tac`(d * (m DIV d)) MOD _` - \\ `m DIV d * d <= m` by ( - DEP_REWRITE_TAC[GSYM X_LE_DIV] \\ fs[Abbr`d`] ) - \\ fs[] - \\ `d * (n DIV d) <= m` by metis_tac[] - \\ pop_assum mp_tac - \\ simp_tac pure_ss [Once MULT_COMM] - \\ DEP_REWRITE_TAC[GSYM X_LE_DIV] - \\ conj_tac >- simp[Abbr`d`] - \\ simp[NOT_LESS_EQUAL] - \\ `d * (m DIV d) < d * (n DIV d)` suffices_by fs[] - \\ metis_tac[]) - Theorem byte_align_IN_IMP_IN_range `byte_align a ∈ dm ∧ (dm = { w | low <=+ w ∧ w <+ hi }) ∧ @@ -2993,55 +2970,6 @@ Theorem byte_align_IN_IMP_IN_range \\ asm_exists_tac \\ fs[alignmentTheory.byte_align_def]); -local - open alignmentTheory - val aligned_add_mult_lemma = Q.prove( - `aligned k (w + n2w (2 ** k)) = aligned k w`, - fs [aligned_add_sub,aligned_pow2]) |> GEN_ALL - val aligned_add_mult_any = Q.prove( - `!n w. aligned k (w + n2w (n * 2 ** k)) = aligned k w`, - Induct \\ fs [MULT_CLAUSES,GSYM word_add_n2w] \\ rw [] - \\ pop_assum (qspec_then `w + n2w (2 ** k)` mp_tac) - \\ fs [aligned_add_mult_lemma]) |> GEN_ALL -in - val aligned_add_pow = save_thm("aligned_add_pow[simp]", - CONJ aligned_add_mult_lemma aligned_add_mult_any) -end - -Theorem align_add_aligned_gen - `∀a. aligned p a ⇒ (align p (a + b) = a + align p b)` - (completeInduct_on`w2n b` - \\ rw[] - \\ Cases_on`w2n b < 2 ** p` - >- ( - simp[alignmentTheory.align_add_aligned] - \\ `align p b = 0w` by simp[lt_align_eq_0] - \\ simp[] ) - \\ fs[NOT_LESS] - \\ Cases_on`w2n b = 2 ** p` - >- ( - `aligned p b` by( - simp[alignmentTheory.aligned_def,alignmentTheory.align_w2n] - \\ metis_tac[n2w_w2n] ) - \\ `aligned p (a + b)` by metis_tac[alignmentTheory.aligned_add_sub_cor] - \\ fs[alignmentTheory.aligned_def]) - \\ fs[LESS_EQ_EXISTS] - \\ qmatch_asmsub_rename_tac`w2n b = z + _` - \\ first_x_assum(qspec_then`z`mp_tac) - \\ impl_keep_tac >- fs[] - \\ `z < dimword(:'a)` by metis_tac[w2n_lt, LESS_TRANS] - \\ disch_then(qspec_then`n2w z`mp_tac) - \\ impl_tac >- simp[] - \\ strip_tac - \\ first_assum(qspec_then`a + n2w (2 ** p)`mp_tac) - \\ impl_tac >- fs[] - \\ rewrite_tac[word_add_n2w, GSYM WORD_ADD_ASSOC] - \\ Cases_on`b` \\ fs[GSYM word_add_n2w] - \\ strip_tac - \\ first_x_assum(qspec_then`n2w (2**p)`mp_tac) - \\ impl_tac >- fs[aligned_w2n] - \\ simp[]); - Theorem MULT_DIV_MULT_LEMMA `!m l k. 0 < m /\ 0 < l ==> (m * k) DIV (l * m) = k DIV l` (rw [] \\ qsuff_tac `k * m DIV (m * l) = k DIV l` THEN1 fs [] From a2cd3fb5afd66702e7ef35a122e030553c69af73 Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Fri, 24 May 2019 18:05:30 +0100 Subject: [PATCH 3/3] Fix a reference to word_bit_test --- compiler/bootstrap/translation/ag32ProgScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/bootstrap/translation/ag32ProgScript.sml b/compiler/bootstrap/translation/ag32ProgScript.sml index 70547d2a78..0d964c6af6 100644 --- a/compiler/bootstrap/translation/ag32ProgScript.sml +++ b/compiler/bootstrap/translation/ag32ProgScript.sml @@ -82,7 +82,7 @@ fun format_def def = def wordsTheory.word_bits_mask,wordsTheory.WORD_MUL_LSL, wordsTheory.word_mul_n2w,addressTheory.word_arith_lemma2, wordsTheory.WORD_LT,word_msb_word_bit,ag32_constant_def, - EVAL ``dimindex (:32)``,miscTheory.word_bit_test] + EVAL ``dimindex (:32)``,wordsTheory.word_bit_test] |> REWRITE_RULE [word_neg]; val r = translate (format_def ag32_jump_constant_def);