From 2cc3f86f4ca5a3a192430d8972534ed556d0457b Mon Sep 17 00:00:00 2001 From: John Harrison Date: Tue, 22 Oct 2024 17:46:51 -0700 Subject: [PATCH] Added several new lemmas for "simple subwords of composite word expressions": WORD_SUBWORD_INSERT_INNER WORD_SUBWORD_INSERT_OUTER WORD_SUBWORD_JOIN_LOWER WORD_SUBWORD_JOIN_UPPER WORD_SUBWORD_SUBWORD WORD_SUBWORD_TRIVIAL as well as a new conversion WORD_SIMPLE_SUBWORD_CONV that packages them up into a simplifying function, e.g. # WORD_SIMPLE_SUBWORD_CONV `word_subword (x:int16) (0,16):int16`;; val it : thm = |- word_subword x (0,16) = x # WORD_SIMPLE_SUBWORD_CONV `word_subword (word_join (x:int16) (y:int16):int32) (0,16):int16`;; val it : thm = |- word_subword (word_join x y) (0,16) = word_subword y (0,16) # WORD_SIMPLE_SUBWORD_CONV `word_subword (word_subword (x:int64) (32,32):int32) (0,16):int16`;; val it : thm = |- word_subword (word_subword x (32,32)) (0,16) = word_subword x (32,16) --- Library/words.ml | 106 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 106 insertions(+) diff --git a/Library/words.ml b/Library/words.ml index a7df19c8..e199aca1 100644 --- a/Library/words.ml +++ b/Library/words.ml @@ -4034,6 +4034,49 @@ let VAL_WORD_SUBWORD_JOIN = prove REWRITE_TAC[MOD_MOD_EXP_MIN] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC]);; +let WORD_SUBWORD_JOIN_LOWER = prove + (`!(h:M word) (l:N word) pos len. + pos + len <= dimindex(:N) /\ dimindex(:N) <= dimindex(:P) + ==> word_subword (word_join (h:M word) (l:N word):P word) + (pos,len):Q word = + word_subword l (pos,len)`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[WORD_EQ_BITS_ALT; BIT_WORD_SUBWORD; BIT_WORD_JOIN] THEN + REPEAT STRIP_TAC THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN + TRY ASM_ARITH_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN + AP_THM_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC);; + +let WORD_SUBWORD_JOIN_UPPER = prove + (`!(h:M word) (l:N word) pos len. + dimindex(:N) <= pos /\ pos + len <= dimindex(:P) + ==> word_subword (word_join (h:M word) (l:N word):P word) + (pos,len):Q word = + word_subword h (pos - dimindex(:N),len)`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[WORD_EQ_BITS_ALT; BIT_WORD_SUBWORD; BIT_WORD_JOIN] THEN + REPEAT STRIP_TAC THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN + TRY ASM_ARITH_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN + BINOP_TAC THEN TRY(AP_THM_TAC THEN AP_TERM_TAC) THEN ASM_ARITH_TAC);; + +let WORD_SUBWORD_SUBWORD = prove + (`!(x:M word) pos1 len1 pos2 len2. + len1 <= dimindex(:N) /\ dimindex(:N) <= dimindex(:M) + ==> word_subword (word_subword x (pos1,len1):N word) + (pos2,len2):P word = + word_subword x (pos1+pos2,MIN len2 (len1-pos2))`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[WORD_EQ_BITS_ALT; BIT_WORD_SUBWORD] THEN + REWRITE_TAC[GSYM ADD_ASSOC] THEN + REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN ASM_REWRITE_TAC[] THEN + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BIT_GUARD]) THEN + ASM_ARITH_TAC);; + +let WORD_SUBWORD_TRIVIAL = prove + (`!(x:N word) n. dimindex(:N) <= n ==> word_subword x (0,n) = x`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[WORD_EQ_BITS_ALT; BIT_WORD_SUBWORD; ADD_CLAUSES] THEN + ASM_SIMP_TAC[ARITH_RULE `N:num <= n ==> MIN n N = N`]);; + let WORD_SUBWORD_DIMINDEX = prove (`!(x:N word) k. word_subword x (k,dimindex(:M)):M word = word_zx(word_ushr x k)`, @@ -4297,6 +4340,69 @@ let BIT_WORD_INSERT = prove REWRITE_TAC[CONG; MOD_MOD_EXP_MIN] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC);; +let WORD_SUBWORD_INSERT_OUTER = prove + (`!(x:M word) (y:N word) pos1 len1 pos2 len2. + pos2 + len2 <= dimindex(:P) /\ + (pos2 + len2 <= pos1 \/ pos1 + len1 <= pos2) + ==> word_subword (word_insert x (pos1,len1) y:P word) + (pos2,len2):Q word = + word_subword x (pos2,len2)`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[WORD_EQ_BITS_ALT; BIT_WORD_SUBWORD; BIT_WORD_INSERT] THEN + REPEAT STRIP_TAC THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN + TRY ASM_ARITH_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN + REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN ASM_REWRITE_TAC[] THEN + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BIT_GUARD]) THEN + ASM_ARITH_TAC);; + +let WORD_SUBWORD_INSERT_INNER = prove + (`!(x:M word) (y:N word) pos1 len1 pos2 len2. + pos2 + len2 <= dimindex(:P) /\ + pos1 <= pos2 /\ pos2 + len2 <= pos1 + len1 + ==> word_subword (word_insert x (pos1,len1) y:P word) + (pos2,len2):Q word = + word_subword y (pos2-pos1,len2)`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[WORD_EQ_BITS_ALT; BIT_WORD_SUBWORD; BIT_WORD_INSERT] THEN + REPEAT STRIP_TAC THEN REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN + TRY ASM_ARITH_TAC THEN REWRITE_TAC[CONJ_ASSOC] THEN + REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN ASM_REWRITE_TAC[] THEN + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [BIT_GUARD]) THEN + TRY ASM_ARITH_TAC THEN REWRITE_TAC[IMP_CONJ] THEN DISCH_TAC THEN + MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC);; + +(* ------------------------------------------------------------------------- *) +(* Reduce some "simple" subword expressions, those that are simply *) +(* equivalent to related ones for subexpresions of the word argument. *) +(* ------------------------------------------------------------------------- *) + +let WORD_SIMPLE_SUBWORD_CONV = + let dimarith_conv = DEPTH_CONV(!word_SIZE_CONV ORELSEC NUM_RED_CONV) in + let dimarith_rule th = + MP th (EQT_ELIM(dimarith_conv(lhand(concl th)))) + and post_rule = + CONV_RULE(RAND_CONV(RAND_CONV(BINOP_CONV dimarith_conv))) in + let [rules_join; rules_insert; rules_subword; [rule_trivial]] = + map (map (PART_MATCH (lhand o rand))) + [[WORD_SUBWORD_JOIN_LOWER; WORD_SUBWORD_JOIN_UPPER]; + [WORD_SUBWORD_INSERT_OUTER; WORD_SUBWORD_INSERT_INNER]; + [WORD_SUBWORD_SUBWORD]; + [WORD_SUBWORD_TRIVIAL]] in + fun tm -> + match tm with + Comb(Comb(Const("word_subword",_),itm), + Comb(Comb(Const(",",_),Comb(Const("NUMERAL",_),_)), + Comb(Const("NUMERAL",_),_))) -> + (match itm with + Comb(Comb(Const("word_join",_),_),_) -> + post_rule(tryfind (fun f -> dimarith_rule(f tm)) rules_join) + | Comb(Comb(Comb(Const("word_insert",_),_),_),_) -> + post_rule(tryfind (fun f -> dimarith_rule(f tm)) rules_insert) + | Comb(Comb(Const("word_subword",_),_),_) -> + post_rule(tryfind (fun f -> dimarith_rule(f tm)) rules_subword) + | _ -> dimarith_rule(rule_trivial tm)) + | _ -> failwith "WORD_SIMPLE_SUBWORD_CONV";; + (* ------------------------------------------------------------------------- *) (* Bit recursion equations for "linear" operations. *) (* ------------------------------------------------------------------------- *)