Skip to content

Commit

Permalink
Added several new lemmas for "simple subwords of composite word
Browse files Browse the repository at this point in the history 
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)
  • Loading branch information
@jargh
jargh committed Oct 23, 2024
1 parent b5e71c0 commit 2cc3f86
Showing 1 changed file with 106 additions and 0 deletions.
106 changes: 106 additions & 0 deletions Library/words.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)`,
Expand Down Expand Up @@ -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. *)
(* ------------------------------------------------------------------------- *)
Expand Down

0 comments on commit 2cc3f86

Please sign in to comment.