Skip to content

Commit

Permalink
Added more word lemmas
Browse files Browse the repository at this point in the history 
        BIT_REVERSEFIELDS_1
        WORD_CLZ_REVERSEFIELDS
        WORD_CTZ_EMULATION_POPCOUNT
        WORD_CTZ_REVERSEFIELDS
        WORD_EVENPARITY_POPCOUNT
        WORD_MUL_EXPAND
        WORD_MUL_EXPAND_ALT
        WORD_ODDPARITY_POPCOUNT
        WORD_POPCOUNT_MUL

as well as defining a couple more utility functions for the word type

        dest_word_ty
        mk_word_ty

and augmenting BIT_WORD_CONV to handle the two special cases of
condition and mask words based on "bitval b":

  BIT_WORD_CONV `bit 0 (word(bitval b):byte)`;;

  BIT_WORD_CONV `bit 42 (word_neg(word(bitval b)):int64)`;;

As for the SAT interface, made the overall GEN_SAT_PROVE, SAT_PROVE and
ZSAT_PROVE initially convert any non-variable atomic formulas into
variables before calling the core procedure. This makes things work on
more general tautologies where the atomic formulas are arbitrary. Also
made a few modernizations to the two README files to better reflect
the current experience with MiniSat and zchaff.
  • Loading branch information
@jrh13
jrh13 committed Mar 2, 2024
1 parent c518278 commit 44c12e0
Show file tree
Hide file tree
Showing 5 changed files with 254 additions and 17 deletions.
90 changes: 84 additions & 6 deletions CHANGES
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,84 @@
* page: https://github.com/jrh13/hol-light/commits/master *
* *****************************************************************

Fri 1st Mar 2024 Library/words.ml

Added a few more miscellaneous word lemmas:

BIT_REVERSEFIELDS_1 =
|- !x i.
bit i (word_reversefields 1 x) <=>
i < dimindex (:N) /\ bit (dimindex (:N) - 1 - i) x

WORD_CLZ_REVERSEFIELDS =
|- !x. word_clz (word_reversefields 1 x) = word_ctz x

WORD_CTZ_EMULATION_POPCOUNT =
|- !x. word_ctz x =
word_popcount (word_and (word_not x) (word_sub x (word 1)))

WORD_CTZ_REVERSEFIELDS =
|- !x. word_ctz (word_reversefields 1 x) = word_clz x

WORD_EVENPARITY_POPCOUNT =
|- !x. word (bitval (word_evenparity x)) =
word_zx (word_not (word (word_popcount x)))

WORD_MUL_EXPAND =
|- !x y.
word_mul x y =
word
(nsum {i | i < dimindex (:N)}
(\i. bitval (bit i x) * val (word_shl y i)))

WORD_MUL_EXPAND_ALT =
|- !x y.
word_mul x y =
word
(nsum {i | i < dimindex (:N)}
(\i. val
(word_and (word_neg (word (bitval (bit i x)))) (word_shl y i))))

WORD_ODDPARITY_POPCOUNT =
|- !x. word (bitval (word_oddparity x)) = word_zx (word (word_popcount x))

WORD_POPCOUNT_MUL =
|- !x y. word_popcount (word_mul x y) <= word_popcount x * word_popcount y

and two new type constructor/destructor utility functions,
"dest_word_ty" and "mk_word_ty", e.g.

# dest_word_ty `:int64`;;
val it : num = 64

Fri 1st Mar 2024 printer.ml

Added a new printing option from June Lee, controlled by a flag
"print_types_of_subterms".

0 - Behaviour as before, no printing of types
1 - prints types of subterms containing invented type variables
2 - prints the types of all constants and variables

Thu 29th Feb 2024 Library/words.ml

Augmented BIT_WORD_CONV to handle the two special cases of condition
and mask words based on "bitval b":

BIT_WORD_CONV `bit 0 (word(bitval b):byte)`;;

BIT_WORD_CONV `bit 42 (word_neg(word(bitval b)):int64)`;;

Tue 27th Feb 2024 Minisat/minisat_prove.ml, Minisat/README, Minisat/zc2mso/README

Made the overall GEN_SAT_PROVE, SAT_PROVE and ZSAT_PROVE initially convert
any non-variable atomic formulas into variables before calling the core
procedure. This makes things work on more general tautologies where the
atomic formulas are arbitrary.

Also made a few modernizations to the two README files to better reflect
the current experience with MiniSat and zchaff.

Wed 21st Feb 2024 EC/jacobian.ml

Added some alternative definitions of Jacobian-coordinate elliptic curve
Expand All @@ -26,7 +104,7 @@ needs to be handled separately:
weierstrass_add (f,a,b)
(weierstrass_of_jacobian f p)
(weierstrass_of_jacobian f q)

WEIERSTRASS_OF_JACOBIAN_DOUBLE_UNEXCEPTIONAL =
|- !f a b p.
field f /\ ~(ring_char f = 2) /\ ~(ring_char f = 3) /\
Expand All @@ -36,7 +114,7 @@ needs to be handled separately:
weierstrass_add (f,a,b)
(weierstrass_of_jacobian f p)
(weierstrass_of_jacobian f p)

Wed 21st Feb 2024 calc_rat.ml, class.ml, define.ml, fusion.ml, int.ml, tactics.ml, Library/words.ml, Help/passim

Added an update from June Lee with two new tactics
Expand All @@ -63,29 +141,29 @@ Added a few additional word lemmas:
FINITE s /\ (!i. i IN s ==> b i < B) /\ (!i. i IN s ==> c i < B)
==> (nsum s (\i. B EXP i * b i) = nsum s (\i. B EXP i * c i) <=>
(!i. i IN s ==> b i = c i))

VAL_EXPAND_SUBWORDS =
|- !k m x.
dimindex (:M) = k /\ dimindex (:N) = k * m
==> nsum {i | i < m}
(\i. 2 EXP (k * i) * val (word_subword x (k * i,k))) =
val x

VAL_SUBWORDS_EQ =
|- !k m f x.
dimindex (:M) = k /\ dimindex (:N) = k * m
==> ((!i. i < m ==> val (word_subword x (k * i,k)) = f i) <=>
(!i. i < m ==> f i < 2 EXP k) /\
val x = nsum {i | i < m} (\i. 2 EXP (k * i) * f i))

WORD_SUBWORD_ADD =
|- !x y.
dimindex (:M) = len /\
pos + len <= dimindex (:N) /\
val x MOD 2 EXP pos + val y MOD 2 EXP pos < 2 EXP pos
==> word_subword (word_add x y) (pos,len) =
word_add (word_subword x (pos,len)) (word_subword y (pos,len))

WORD_SUBWORDS_EQ =
|- !k m f x.
dimindex (:M) = k /\ dimindex (:N) = k * m
Expand Down
129 changes: 124 additions & 5 deletions Library/words.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,7 @@ let DIGITSUM_DIV_MOD = prove
REWRITE_TAC[SING_GSPEC; NSUM_SING; SUB_REFL; MULT_CLAUSES; EXP]);;

let DIGITSUM_UNIQUE = prove
(`!B b c s n.
(`!B b c s.
FINITE s /\
(!i. i IN s ==> b i < B) /\
(!i. i IN s ==> c i < B)
Expand Down Expand Up @@ -405,6 +405,17 @@ let WORD_EQ_BITVECTOR = prove
(`!v w:N word. v = w <=> bitvector v = bitvector w`,
MESON_TAC[word_tybij]);;

(* ------------------------------------------------------------------------- *)
(* Destructors and constructors for the N-bit word type from nums. *)
(* ------------------------------------------------------------------------- *)

let dest_word_ty ty =
match ty with
Tyapp("word",[n]) -> dest_finty n
| _ -> failwith "dest_word_ty";;

let mk_word_ty n = mk_type("word",[mk_finty n]);;

(* ------------------------------------------------------------------------- *)
(* Set up some specific sizes that we want. *)
(* ------------------------------------------------------------------------- *)
Expand Down Expand Up @@ -882,7 +893,7 @@ let BIT_WORD_BITVAL = prove
COND_CASES_TAC THEN REWRITE_TAC[BIT_WORD_0; BIT_WORD_1]);;

let WORD_OF_BITS_SING_AS_WORD_1 = prove
(`!s i. word_of_bits {0}:N word = word 1`,
(`word_of_bits {0}:N word = word 1`,
REWRITE_TAC[WORD_OF_BITS_SING_AS_WORD; EXP]);;

let BITS_OF_WORD_1 = prove
Expand Down Expand Up @@ -2722,6 +2733,18 @@ let WORD_SHL_IWORD = prove
`(x:int == y) (mod p) ==> (x * n == n * y) (mod p)`) THEN
REWRITE_TAC[IVAL_IWORD_CONG]);;

let WORD_MUL_EXPAND = prove
(`!x y:N word.
word_mul x y =
word(nsum {i | i < dimindex(:N)}
(\i. bitval(bit i x) * val(word_shl y i)))`,
REPEAT GEN_TAC THEN REWRITE_TAC[word_mul; modular] THEN
GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [val_def] THEN
REWRITE_TAC[GSYM VAL_EQ; VAL_WORD; GSYM NSUM_RMUL; NUMSEG_LT_DIMINDEX] THEN
ONCE_REWRITE_TAC[MOD_NSUM_MOD_NUMSEG] THEN
REWRITE_TAC[VAL_WORD_SHL] THEN CONV_TAC MOD_DOWN_CONV THEN
REWRITE_TAC[MULT_AC]);;

let word_ushr = new_definition
`word_ushr (x:(N)word) n =
word((val x) DIV (2 EXP n)):(N)word`;;
Expand Down Expand Up @@ -5085,6 +5108,17 @@ let REAL_VAL_WORD_MASK = prove
COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN
REAL_ARITH_TAC);;

let WORD_MUL_EXPAND_ALT = prove
(`!x y:N word.
word_mul x y =
word(nsum {i | i < dimindex(:N)}
(\i. val(word_and (word_neg(word(bitval(bit i x))))
(word_shl y i))))`,
REPEAT GEN_TAC THEN REWRITE_TAC[WORD_MUL_EXPAND] THEN
AP_TERM_TAC THEN MATCH_MP_TAC NSUM_EQ THEN REPEAT STRIP_TAC THEN
REWRITE_TAC[WORD_AND_MASK] THEN COND_CASES_TAC THEN
ASM_REWRITE_TAC[BITVAL_CLAUSES; MULT_CLAUSES; WORD_VAL; VAL_WORD_0]);;

let WORD_SX_ZX_GEN = prove
(`!x. (word_sx:M word->N word) x =
word_or (word_shl (word_neg(word(bitval(bit (dimindex(:M)-1) x))))
Expand Down Expand Up @@ -5203,12 +5237,12 @@ let MASK_WORD_SUB = prove
REWRITE_TAC[EXP_EQ_0; ARITH_EQ]);;

let WORD_AND_MASK_WORDS = prove
(`!i j. word_and (word(2 EXP j - 1)) (word(2 EXP k - 1)):N word =
(`!j k. word_and (word(2 EXP j - 1)) (word(2 EXP k - 1)):N word =
word(2 EXP MIN j k - 1)`,
SIMP_TAC[WORD_EQ_BITS_ALT; BIT_WORD_AND; BIT_MASK_WORD] THEN ARITH_TAC);;

let WORD_OR_MASK_WORDS = prove
(`!i j. word_or (word(2 EXP j - 1)) (word(2 EXP k - 1)):N word =
(`!j k. word_or (word(2 EXP j - 1)) (word(2 EXP k - 1)):N word =
word(2 EXP MAX j k - 1)`,
SIMP_TAC[WORD_EQ_BITS_ALT; BIT_WORD_OR; BIT_MASK_WORD] THEN ARITH_TAC);;

Expand Down Expand Up @@ -5651,6 +5685,23 @@ let WORD_CLZ_MONO = prove
`(!d:num. d <= x ==> d <= y) ==> x <= y`) THEN
REWRITE_TAC[WORD_LE_CLZ_VAL] THEN ASM_ARITH_TAC);;

let WORD_CTZ_EMULATION_POPCOUNT = prove
(`!x:N word.
word_ctz x =
word_popcount(word_and (word_not x) (word_sub x (word 1)))`,
GEN_TAC THEN ASM_CASES_TAC `x:N word = word 0` THEN
ASM_REWRITE_TAC[word_ctz; WORD_AND_REFL; WORD_POPCOUNT_NOT;
WORD_POPCOUNT_0; SUB_0; WORD_RULE
`word_sub (word 0) (word 1) = word_not(word 0)`] THEN
REWRITE_TAC[word_popcount; bits_of_word; BIT_WORD_AND_NOT_SUB_1] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [WORD_EQ_BITS]) THEN
REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; BIT_WORD_0] THEN
GEN_REWRITE_TAC LAND_CONV [MINIMAL] THEN
ABBREV_TAC `m = minimal i. bit i (x:N word)` THEN POP_ASSUM(K ALL_TAC) THEN
STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM CARD_NUMSEG_LT] THEN
AP_TERM_TAC THEN REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
ASM_MESON_TAC[BIT_GUARD; LTE_TRANS; LT_TRANS; LE_REFL; NOT_LE]);;

(* ------------------------------------------------------------------------- *)
(* Reversal of the b-bit fields in an N-bit word. If N isn't a multiple *)
(* of b, this leaves bits above the highest b multiple unchanged. *)
Expand Down Expand Up @@ -5703,6 +5754,32 @@ let WORD_REVERSEFIELDS_REVERSEFIELDS = prove
MATCH_MP_TAC(ARITH_RULE `x < n ==> n - 1 - (n - 1 - x) = x`) THEN
ASM_SIMP_TAC[RDIV_LT_EQ; LE_1] THEN ASM_ARITH_TAC]);;

let BIT_REVERSEFIELDS_1 = prove
(`!(x:N word) i.
bit i (word_reversefields 1 x) <=>
i < dimindex(:N) /\ bit (dimindex(:N) - 1 - i) x`,
REPEAT GEN_TAC THEN REWRITE_TAC[BIT_WORD_REVERSEFIELDS] THEN
REWRITE_TAC[MULT_CLAUSES; DIV_1; MOD_1; ADD_CLAUSES] THEN
MESON_TAC[]);;

let WORD_CTZ_REVERSEFIELDS = prove
(`!x:N word. word_ctz(word_reversefields 1 x) = word_clz x`,
GEN_TAC THEN REWRITE_TAC[MESON[LE_REFL; LE_ANTISYM]
`a = b <=> !x:num. x <= a <=> x <= b`] THEN
REWRITE_TAC[WORD_LE_CTZ; WORD_LE_CLZ] THEN
X_GEN_TAC `k:num` THEN REWRITE_TAC[BIT_REVERSEFIELDS_1] THEN
MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN
DISCH_TAC THEN EQ_TAC THEN DISCH_TAC THEN
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC `dimindex(:N) - 1 - i`) THEN
FIRST_X_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [BIT_GUARD]) THEN
ASM_SIMP_TAC[ARITH_RULE `i < n ==> n - 1 - (n - 1 - i) = i`] THEN
ASM_ARITH_TAC);;

let WORD_CLZ_REVERSEFIELDS = prove
(`!x:N word. word_clz(word_reversefields 1 x) = word_ctz x`,
MESON_TAC[WORD_REVERSEFIELDS_REVERSEFIELDS; WORD_CTZ_REVERSEFIELDS]);;

(* ------------------------------------------------------------------------- *)
(* Byte reversal, with type constrained to multiple of 8. *)
(* ------------------------------------------------------------------------- *)
Expand Down Expand Up @@ -6171,7 +6248,12 @@ let BIT_WORD_CONV =
and zero_tm = `0` and one_tm = `1` in
fun tm ->
match tm with
Comb(Comb(Const("bit",_),n),Comb(Const("word",_),m))
Comb(Comb(Const("bit",_),n),
Comb(Const("word",_),Comb(Const("bitval",_),_)))
when is_numeral n ->
(GEN_REWRITE_CONV I [BIT_WORD_BITVAL] THENC
LAND_CONV NUM_EQ_CONV THENC conv_and) tm
| Comb(Comb(Const("bit",_),n),Comb(Const("word",_),m))
when is_numeral n && is_numeral m ->
if m = zero_tm then
GEN_REWRITE_CONV I [BIT_WORD_0] tm
Expand Down Expand Up @@ -6217,6 +6299,13 @@ let BIT_WORD_CONV =
(GEN_REWRITE_CONV I [rule_sub (num_CONV n)] THENC
LAND_CONV(RAND_CONV(!word_SIZE_CONV) THENC NUM_LT_CONV) THENC
conv_and) tm
| Comb(Comb(Const("bit",_),n),
Comb(Const("word_neg",_),
Comb(Const("word",_),Comb(Const("bitval",_),_))))
when is_numeral n ->
(GEN_REWRITE_CONV I [BIT_WORD_MASK] THENC
LAND_CONV (RAND_CONV(!word_SIZE_CONV) THENC NUM_LT_CONV) THENC
conv_and) tm
| Comb(Comb(Const("bit",_),n),Comb(Const("word_neg",_),_))
when is_numeral n ->
if n = zero_tm then
Expand Down Expand Up @@ -6475,6 +6564,36 @@ let WORD_POPCOUNT_ADD = prove
word_popcount(word_add x y) <= word_popcount x + word_popcount y`,
MESON_TAC[LE_TRANS; WORD_POPCOUNT_ADD_OR; WORD_POPCOUNT_OR]);;

let WORD_POPCOUNT_MUL = prove
(`!x y:N word.
word_popcount(word_mul x y) <= word_popcount x * word_popcount y`,
REPEAT GEN_TAC THEN REWRITE_TAC[WORD_MUL_EXPAND_ALT] THEN
GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [WORD_POPCOUNT_NSUM] THEN
SPEC_TAC(`dimindex(:N)`,`n:num`) THEN MATCH_MP_TAC num_INDUCTION THEN
REWRITE_TAC[CONJUNCT1 LT; NSUM_CLAUSES_NUMSEG_LT] THEN
REWRITE_TAC[WORD_POPCOUNT_0; MULT_CLAUSES; LE_REFL] THEN
X_GEN_TAC `n:num` THEN DISCH_TAC THEN REWRITE_TAC[WORD_ADD] THEN
W(MP_TAC o PART_MATCH lhand WORD_POPCOUNT_ADD o lhand o snd) THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] LE_TRANS) THEN
REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN MATCH_MP_TAC LE_ADD2 THEN
ASM_REWRITE_TAC[WORD_VAL] THEN REWRITE_TAC[WORD_AND_MASK] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES; BITVAL_CLAUSES] THEN
REWRITE_TAC[WORD_POPCOUNT_0; LE_REFL; WORD_POPCOUNT_SHL]);;

let WORD_ODDPARITY_POPCOUNT = prove
(`!x:N word. word(bitval(word_oddparity x)):M word =
word_zx(word(word_popcount x):1 word)`,
GEN_TAC THEN REWRITE_TAC[word_oddparity] THEN
ONCE_REWRITE_TAC[WORD_BLAST `x:1 word = word(bitval(bit 0 x))`] THEN
REWRITE_TAC[WORD_ZX_BITVAL; BIT_LSB_WORD]);;

let WORD_EVENPARITY_POPCOUNT = prove
(`!x:N word. word(bitval(word_evenparity x)):M word =
word_zx(word_not(word(word_popcount x)):1 word)`,
REPEAT GEN_TAC THEN REWRITE_TAC[word_evenparity; GSYM NOT_ODD] THEN
ONCE_REWRITE_TAC[WORD_BLAST `x:1 word = word(bitval(bit 0 x))`] THEN
REWRITE_TAC[WORD_ZX_BITVAL; BIT_WORD_NOT; DIMINDEX_1; ARITH; BIT_LSB_WORD]);;

(* ------------------------------------------------------------------------- *)
(* Conversions for explicit calculations with terms of the form "word n" *)
(* where n is a numeral. They all work for arbitrary n and whenever they *)
Expand Down
12 changes: 12 additions & 0 deletions Minisat/README
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,18 @@ proof-logging version "MiniSat-p" installed. For downloads, see:

http://minisat.se/MiniSat.html

The recommended version is this one, specifically:

http://minisat.se/downloads/MiniSat-p_v1.14.2006-Sep-07.src.zip

I found that there can be a few problems compiling MiniSat with
modern C++ compilers (specifically g++ version 13), possibly
solved by:

* Replacing "uint" with "uint32_t"

* Replacing instances of "throw(whatever)" by "noexcept(false)"

By default, the code will look for MiniSat on your PATH. If it
doesn't find it, you can explicitly indicate the directory that
contains the MiniSat binary by changing the assignment of the
Expand Down
Loading

0 comments on commit 44c12e0

Please sign in to comment.