From c153f40da8deb3bcc7aaef39126ad15e4713e68c Mon Sep 17 00:00:00 2001 From: John Harrison Date: Wed, 20 Mar 2024 00:56:16 +0000 Subject: [PATCH] Added a basic bit-blasting tactic and rule to the word library, using BDDs as the backend by default (BITBLAST_TAC and BITBLAST_RULE) but providing a more general BITBLAST_THEN that does the reduction followed by another tactic (e.g. SAT). The new file "Examples/bitblast.ml" gives a number of examples, mainly typical "Hacker's Delight" fare. Added a proof of Bondy's theorem, following the first of the two proofs given in Bollobas's "Combinatorics" for Theorem 1 (p4). Made "strings_of_file" and "string_of_file" more robust so they can handle bigger input files without problems. Previously, the core loop of "strings_of_file" was not tail recursive because the body was enclosed in a "try...with" block; this is now changed. The "string_of_file" function now just uses more basic library functions directly instead of calling "strings_of_file" and concatenating the results. --- CHANGES | 22 ++ Examples/bitblast.ml | 517 +++++++++++++++++++++++++++++++++++++++++++ Examples/bondy.ml | 70 ++++++ Library/words.ml | 324 ++++++++++++++++++++++++++- holtest | 2 + holtest.mk | 2 + lib.ml | 17 +- 7 files changed, 943 insertions(+), 11 deletions(-) create mode 100644 Examples/bitblast.ml create mode 100644 Examples/bondy.ml diff --git a/CHANGES b/CHANGES index ce2ad450..540477f1 100644 --- a/CHANGES +++ b/CHANGES @@ -8,6 +8,28 @@ * page: https://github.com/jrh13/hol-light/commits/master * * ***************************************************************** +Tue 19th Mar 2024 lib.ml + +Made "strings_of_file" and "string_of_file" more robust so they can handle +bigger input files without problems. Previously, the core loop of +"strings_of_file" was not tail recursive because the body was enclosed in +a "try...with" block; this is now changed. The "string_of_file" function now +just uses more basic library functions directly instead of calling +"strings_of_file" and concatenating the results. + +Mon 18th Mar 2024 Library/words.ml, Examples/bitblast.ml [new file] + +Added a basic bit-blasting tactic and rule to the word library, using +BDDs as the backend by default (BITBLAST_TAC and BITBLAST_RULE) but +providing a more general BITBLAST_THEN that does the reduction followed +by another tactic (e.g. SAT). The new file "Examples/bitblast.ml" gives +a number of examples, mainly typical "Hacker's Delight" fare. + +Sat 16th Mar 2024 Examples/bondy.ml [new file] + +Added a new example, a proof of Bondy's theorem, following the first +of the two proofs given in Bollobas's "Combinatorics" for Theorem 1 (p4). + Fri 15th Mar 2024 Library/bdd.ml [new file], Examples/bdd_examples.ml [new file] Added a new file giving a basic implementation (as a HOL derived rule) of diff --git a/Examples/bitblast.ml b/Examples/bitblast.ml new file mode 100644 index 00000000..8103cdd7 --- /dev/null +++ b/Examples/bitblast.ml @@ -0,0 +1,517 @@ +(* ========================================================================= *) +(* Examples of proving properties of machine words via bit-blasting. *) +(* ========================================================================= *) + +needs "Library/words.ml";; + +(* ------------------------------------------------------------------------- *) +(* Wrapper that also expands bounded quantifiers first. *) +(* ------------------------------------------------------------------------- *) + +let BITBLAST tm = + let th = (ONCE_DEPTH_CONV EXPAND_CASES_CONV THENC NUM_REDUCE_CONV) tm in + EQ_MP (SYM th) (BITBLAST_RULE (rand(concl th)));; + +(* ------------------------------------------------------------------------- *) +(* For more data, also use the SAT interface and compare with BDD default. *) +(* ------------------------------------------------------------------------- *) + +(**** + +needs "Minisat/make.ml";; + +let BITBLAST_BDD tm = + let th = (ONCE_DEPTH_CONV EXPAND_CASES_CONV THENC NUM_REDUCE_CONV) tm in + EQ_MP (SYM th) (BITBLAST_RULE (rand(concl th))) +and BITBLAST_MINISAT tm = + let th = (ONCE_DEPTH_CONV EXPAND_CASES_CONV THENC NUM_REDUCE_CONV) tm in + let th' = prove(rand(concl th),BITBLAST_THEN (CONV_TAC o K SAT_PROVE)) in + EQ_MP (SYM th) th' +and BITBLAST_ZCHAFF tm = + let th = (ONCE_DEPTH_CONV EXPAND_CASES_CONV THENC NUM_REDUCE_CONV) tm in + let th' = prove(rand(concl th),BITBLAST_THEN (CONV_TAC o K ZSAT_PROVE)) in + EQ_MP (SYM th) th';; + +let BITBLAST tm = + let th1 = (*** Already reports time ***) BITBLAST_BDD tm in + let th2 = time BITBLAST_MINISAT tm in + let th3 = time BITBLAST_ZCHAFF tm in + if concl th1 = tm && concl th2 = tm && concl th3 = tm + then th1 else failwith "BITBLAST: Sanity check failure";; + +*****) + +(* ------------------------------------------------------------------------- *) +(* Some easy examples. *) +(* ------------------------------------------------------------------------- *) + +BITBLAST `word_xor x y:int64 = word_sub (word_or x y) (word_and x y)`;; + +BITBLAST + `word_add x y:int64 = word_sub (word_shl (word_or x y) 1) (word_xor x y)`;; + +BITBLAST + `word_and (word_not x) (word_sub x (word 1)):int64 = + word_not (word_or x (word_neg x))`;; + +BITBLAST + `word_not (word_or x (word_neg x)):int64 = + word_sub (word_and x (word_neg x)) (word 1)`;; + +(* ------------------------------------------------------------------------- *) +(* Ways of getting a carry flag post-hoc. *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!x y:int64. + val(word_add x y) < val x <=> ~(val(word_add x y) = val(x) + val(y))`;; + +BITBLAST + `!x y:int64. + val(word_add x y) >= val y <=> val(word_add x y) = val(x) + val(y)`;; + +(* ------------------------------------------------------------------------- *) +(* Sign extension from Hacker's Delight 2.5 *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `word_sub (word_xor ((word_zx:int32->int64) x) (word 0x80000000)) + (word 0x80000000) = + word_sx x`;; + +(* ------------------------------------------------------------------------- *) +(* Sign swaps, from http://graphics.stanford.edu/~seander/bithacks.html *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `let m:int64 = word_neg(word(bitval b)) in + word_sub (word_xor x m) m = word_xor (word_add x m) m`;; + +(* ------------------------------------------------------------------------- *) +(* Getting a mask or C condition for a zero test. *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!x:int64. + (word_ushr (word_or (word_neg x) x) 63 = word 1 <=> ~(x = word 0)) /\ + (word_ushr (word_or (word_neg x) x) 63 = word 0 <=> x = word 0)`;; + +BITBLAST + `!x:int64. + (word_ishr (word_or (word_neg x) x) 63 = word 0xFFFFFFFFFFFFFFFF <=> + ~(x = word 0)) /\ + (word_ishr (word_or (word_neg x) x) 63 = word 0 <=> x = word 0)`;; + +(* ------------------------------------------------------------------------- *) +(* Computing popcount. *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!x:int64. + let x2 = word_sub x (word_ushr (word_and x (word 0xAAAAAAAAAAAAAAAA)) 1) in + let x4 = word_add (word_and x2 (word 0x3333333333333333)) + (word_ushr (word_and x2 (word 0xCCCCCCCCCCCCCCCC)) 2) in + let x8 = word_and (word_add x4 (word_ushr x4 4)) + (word 0x0F0F0F0F0F0F0F0F) in + let x64 = word_mul x8 (word 0x101010101010101) in + let y = word_ushr x64 56 in + y = word(word_popcount x)`;; + +BITBLAST + `!x:15 word. + let u:int64 = word_mul (word_zx x) (word 0x0002000400080010) in + let v = word_and u (word 0x1111111111111111) in + let w = word_mul v (word 0x1111111111111111) in + let y = word_ushr w 60 in + y = word(word_popcount x)`;; + +(* ------------------------------------------------------------------------- *) +(* Primality checking. *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!x:nybble y:nybble. val x * val y = 13 ==> val x = 1 \/ val y = 1`;; + +BITBLAST + `!x:byte y:byte. val x * val y = 241 ==> val x = 1 \/ val y = 1`;; + +(* ------------------------------------------------------------------------- *) +(* Parity. See Hacker's Delight 5-2. *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!x:int64. + let x1 = word_xor x (word_ushr x 1) in + let x2 = word_xor x1 (word_ushr x1 2) in + let x4 = word_xor x2 (word_ushr x2 4) in + let x8 = word_xor x4 (word_ushr x4 8) in + let x16 = word_xor x8 (word_ushr x8 16) in + let x32 = word_xor x16 (word_ushr x16 32) in + let y = word_and x32 (word 1) in + y = word(bitval(word_oddparity x))`;; + +BITBLAST + `!x:int32. + let x1 = word_xor x (word_ushr x 1) in + let x2 = word_and (word_xor x1 (word_ushr x1 2)) (word 0x11111111) in + let x4 = word_mul x2 (word 0x11111111) in + let y = word_and (word_ushr x4 28) (word 1) in + y = word(bitval(word_oddparity x))`;; + +BITBLAST + `!x:int32. + let x1 = word_xor x (word_ushr x 1) in + let x2 = word_and (word_xor x1 (word_ushr x1 2)) (word 0x11111111) in + let x4 = word_mul x2 (word 0x88888888) in + let y = word_ushr x4 31 in + y = word(bitval(word_oddparity x))`;; + +(* ------------------------------------------------------------------------- *) +(* Non-overflowing average *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!x y:int64. + word_ushr (word_add (word_zx x) (word_zx y)) 1 :65 word = + word_zx (word_add (word_and x y) (word_ushr (word_xor x y) 1))`;; + +BITBLAST + `!x y:int64. + word_ushr (word_add (word_zx x) (word_zx y)) 1 :int128 = + word_zx (word_add (word_and x y) (word_ushr (word_xor x y) 1))`;; + +BITBLAST + `!x y:int64. + word_ushr (word_add (word_zx x) (word_zx y)) 1 :65 word = + word_zx (word_add (word_add (word_ushr x 1) (word_ushr y 1)) + (word_and (word_and x y) (word 1)))`;; + +(* ------------------------------------------------------------------------- *) +(* Isolating lowest 0 bit ("Matters Computational", 1.3.1). *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!x:int64. let x' = word_not x in + word_and x' (word_neg x') = + word_and (word_xor x (word_add x (word 1))) (word_not x)`;; + +(* ------------------------------------------------------------------------- *) +(* Gray codes are injective. *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `let gray = \x:int64. word_xor x (word_ushr x 1) in + gray x = gray y ==> x = y`;; + +(* ------------------------------------------------------------------------- *) +(* Gray code parity is the same as the LSB of the input. *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `let gray = \x:int64. word_xor x (word_ushr x 1) in + word(bitval(word_oddparity(gray x))):byte = + word(bitval(bit 0 x))`;; + +(* ------------------------------------------------------------------------- *) +(* Recognizing powers of 2 (or zero). *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `word_and x (word_sub x (word 1)):int64 = word 0 <=> + word_and (word(word_popcount x):byte) (word_not(word 1)) = word 0`;; + +BITBLAST + `word_and x (word_sub x (word 1)):int64 = word 0 <=> + word_popcount x = 0 \/ word_popcount x = 1`;; + +(* ------------------------------------------------------------------------- *) +(* Adjacent Gray codes differ in one bit (several formulations). *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `let gray = \x:int64. word_xor x (word_ushr x 1) + and pow2orzero = \x:int64. word_and x (word_sub x (word 1)) = word 0 in + pow2orzero(word_xor (gray x) (gray (word_add x (word 1))))`;; + +BITBLAST + `let gray = \x:int64. word_xor x (word_ushr x 1) + and pow2 = \x:int64. word_and x (word_sub x (word 1)) = word 0 /\ + ~(x = word 0) in + pow2(word_xor (gray x) (gray (word_add x (word 1))))`;; + +BITBLAST + `let gray = \x:int64. word_xor x (word_ushr x 1) in + word(word_popcount(word_xor (gray x) (gray (word_add x (word 1))))):byte = + word 1`;; + +(* ------------------------------------------------------------------------- *) +(* Iterated application of Gray code. *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `let gray = \x:int64. word_xor x (word_ushr x 1) in + gray(gray x) = word_xor x (word_ushr x 2)`;; + +BITBLAST + `let gray = \x:byte. word_xor x (word_ushr x 1) in + gray(gray(gray(gray(gray(gray(gray(gray x))))))) = x`;; + +(* ------------------------------------------------------------------------- *) +(* Something involving the more complicated constructs. *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!x y:int64. word_clz(word_or x y) <= word_clz x`;; + +BITBLAST + `!x:int32. word_popcount(word_add x (word 1)) = 1 + ==> word_ctz x = 0 \/ word_ctz x = 32`;; + +BITBLAST + `!x:int32. ~(x = word 0) + ==> word_popcount(word_sub x (word 1)) + 1 = + word_popcount x + word_ctz x`;; + +BITBLAST + `!x:int32. word_clz x + word_popcount x + word_ctz x = 32 <=> + ~(x = word 0) /\ + word_and (word_add (word_or x (word_sub x (word 1))) (word 1)) x = + word 0`;; + +BITBLAST + `!x:int32. word_popcount x = 0 \/ word_popcount x = 1 <=> + word_and x (word_sub x (word 1)) = word 0`;; + +BITBLAST + `!x:int32. word_popcount x = 1 <=> + word_or (word_not(word_ishr (word_or x (word_neg x)) 31)) + (word_and x (word_sub x (word 1))) = + word 0`;; + +(* ------------------------------------------------------------------------- *) +(* Alternative emulation for ctz in terms of popcount. *) +(* ------------------------------------------------------------------------- *) + +(*** + http://aggregate.org/MAGIC/#SIMD%20Within%20A%20Register%20(SWAR)%20Operations + ***) + +BITBLAST + `!x:int32. word(word_ctz x):byte = + word(word_popcount(word_sub (word_and x (word_neg x)) (word 1)))`;; + +BITBLAST + `!x:int64. word(word_ctz x):byte = + word(word_popcount(word_sub (word_and x (word_neg x)) (word 1)))`;; + +(* ------------------------------------------------------------------------- *) +(* Comparing leading zero counts (Hacker's Delight again). *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!x y:int64. + word_clz x = word_clz y <=> val(word_xor x y) <= val(word_and x y)`;; + +BITBLAST + `!x y:int64. + word_clz x < word_clz y <=> val(word_and x (word_not y)) > val y`;; + +BITBLAST + `!x y:int64. + word_clz x <= word_clz y <=> val(word_and (word_not x) y) <= val x`;; + +(* ------------------------------------------------------------------------- *) +(* Basic SWAR byte operations. Somewhat well-known methods, e.g. *) +(* https://www.chessprogramming.org/SIMD_and_SWAR_Techniques *) +(* ------------------------------------------------------------------------- *) + +(*** Addition ***) + +BITBLAST + `!x y:int64. + let h = word 0x8080808080808080 + and l = word 0x0101010101010101 in + let s = word_add (word_and x (word_not h)) (word_and y (word_not h)) + and t = word_and (word_xor x y) h in + let z = word_xor s t in + !i. i < 8 ==> word_subword z (8*i,8) :byte = + word_add (word_subword x (8*i,8)) (word_subword y (8*i,8))`;; + +(*** Subtraction ***) + +BITBLAST + `!x y:int64. + let h = word 0x8080808080808080 + and l = word 0x0101010101010101 in + let s = word_sub (word_or x h) (word_and y (word_not h)) + and t = word_and (word_xor x (word_not y)) h in + let z = word_xor s t in + !i. i < 8 ==> word_subword z (8*i,8) :byte = + word_sub (word_subword x (8*i,8)) (word_subword y (8*i,8))`;; + +(*** Average ***) + +BITBLAST + `!x y:int64. + let l = word 0x0101010101010101 in + let z = word_add (word_and x y) + (word_ushr (word_and (word_xor x y) (word_not l)) 1) in + !i. i < 8 + ==> word_zx (word_subword z (8*i,8) :byte):9 word = + word_ushr (word_add (word_zx (word_subword x (8*i,8) :byte)) + (word_zx (word_subword y (8*i,8) :byte))) 1`;; + +(* ------------------------------------------------------------------------- *) +(* SWAR comparison. *) +(* https://tldp.org/HOWTO/Parallel-Processing-HOWTO-4.html *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!x y:int64. + let m = word 0x7F7F7F7F7F7F7F7F in + let d = word_xor x y in + let w = word_add (word_and d m) m in + let z = word_not (word_or (word_or d m) w) in + !i. i < 8 + ==> (word_subword z (8*i,8) :byte = word 0 <=> + ~(word_subword x (8*i,8):byte = word_subword y (8*i,8))) /\ + (word_subword z (8*i,8) :byte = word 0x80 <=> + word_subword x (8*i,8):byte = word_subword y (8*i,8))`;; + +BITBLAST + `!x y:int64. + let h = word 0x8080808080808080 in + let d = word_xor x y in + let w = word_and (word_sub (word_or (word_ushr d 1) h) d) h in + let z = word_sub (word_shl w 1) (word_ushr w 7) in + !i. i < 8 + ==> (word_subword z (8*i,8) :byte = word 0 <=> + ~(word_subword x (8*i,8):byte = word_subword y (8*i,8))) /\ + (word_subword z (8*i,8) :byte = word 0xFF <=> + word_subword x (8*i,8):byte = word_subword y (8*i,8))`;; + +BITBLAST + `!x y:int64. + let h = word 0x8080808080808080 in + let m = word_not h in + let d = word_xor x y in + let w = word_add (word_and d m) m in + let z = word_and (word_or w d) h in + !i. i < 8 + ==> (word_subword z (8*i,8) :byte = word 0 <=> + word_subword x (8*i,8):byte = word_subword y (8*i,8)) /\ + (word_subword z (8*i,8) :byte = word 0x80 <=> + ~(word_subword x (8*i,8):byte = word_subword y (8*i,8)))`;; + +(* ------------------------------------------------------------------------- *) +(* Alan Mycroft's test for a zero byte (Knuth 7.1.3, formula 90). *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `let h = word 0x8080808080808080 + and l = word 0x0101010101010101 in + word_and h (word_and (word_sub x l) (word_not x)):int64 = word 0 <=> + !i. i < 8 + ==> ~(word_subword x (8*i,8) :byte = word 0)`;; + +(* ------------------------------------------------------------------------- *) +(* Validity checking for packed BCD *) +(* https://homepage.divms.uiowa.edu/~jones/bcd/bcd.html *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!a:int32. + let w = word_xor (word_add a (word 0x06666666)) a in + let z = word_and w (word 0x11111110) in + ((!i. i < 7 + ==> val(word_subword a (4*i,4):nybble) < 10) + <=> z = word 0)`;; + +(*** A variant including the top digit in the check ***) + +BITBLAST + `!a:int32. + let a' = word_ushr a 1 in + let w = word_xor (word_add a' (word 0x33333333)) a' in + let z = word_and w (word 0x88888888) in + ((!i. i < 8 + ==> val(word_subword a (4*i,4):nybble) < 10) + <=> z = word 0)`;; + +(* ------------------------------------------------------------------------- *) +(* Modular inverse approximation magic *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!a:5 word. + let x = word_xor (word_sub a (word_shl a 2)) (word 2) in + bit 0 a ==> word_mul a x = word_neg(word 1)`;; + +BITBLAST + `!a:4 word. + let x = word_sub (word_shl (word_and (word_sub (word 1) a) (word 4)) 1) a in + bit 0 a ==> word_mul a x = word_neg(word 1)`;; + +(* ------------------------------------------------------------------------- *) +(* Various ways of counting leading zeros - Hacker's Delight 5-15 etc. *) +(* ------------------------------------------------------------------------- *) + +BITBLAST + `!x:int64. + let x1 = word_or x (word_ushr x 1) in + let x2 = word_or x1 (word_ushr x1 2) in + let x4 = word_or x2 (word_ushr x2 4) in + let x8 = word_or x4 (word_ushr x4 8) in + let x16 = word_or x8 (word_ushr x8 16) in + let x32 = word_or x16 (word_ushr x16 32) in + word_popcount(word_not x32) = word_clz x`;; + +BITBLAST + `!x:int64. + let x1 = word_or x (word_ushr x 32) in + let x2 = word_or x1 (word_ushr x1 16) in + let x4 = word_or x2 (word_ushr x2 8) in + let x8 = word_or x4 (word_ushr x4 4) in + let x16 = word_or x8 (word_ushr x8 2) in + let x32 = word_or x16 (word_ushr x16 1) in + word_popcount(word_not x32) = word_clz x`;; + +BITBLAST + `!x:int64. + (if x = word 0 then word 64 else + let n = word 0 in + let x0,n0 = if val x <= 0x00000000FFFFFFFF + then word_shl x 32,word_add n (word 32) else x,n in + let x1,n1 = if val x0 <= 0x0000FFFFFFFFFFFF + then word_shl x0 16,word_add n0 (word 16) else x0,n0 in + let x2,n2 = if val x1 <= 0x00FFFFFFFFFFFFFF + then word_shl x1 8,word_add n1 (word 8) else x1,n1 in + let x3,n3 = if val x2 <= 0x0FFFFFFFFFFFFFFF + then word_shl x2 4,word_add n2 (word 4) else x2,n2 in + let x4,n4 = if val x3 <= 0x3FFFFFFFFFFFFFFF + then word_shl x3 2,word_add n3 (word 2) else x3,n3 in + if val x4 <= 0x7FFFFFFFFFFFFFFF then word_add n4 (word 1) else n4):int64 = + word(word_clz x)`;; + +BITBLAST + `!x:int64. + let MASK32 = word 0xFFFFFFFF00000000 + and MASK16 = word 0xFFFF0000FFFF0000 + and MASK8 = word 0xFF00FF00FF00FF00 + and MASK4 = word 0xF0F0F0F0F0F0F0F0 + and MASK2 = word 0xCCCCCCCCCCCCCCCC + and MASK1 = word 0xAAAAAAAAAAAAAAAA in + (if x = word 0 then 64 else + (if val(word_and x MASK32) < val(word_and x (word_not MASK32)) + then 32 else 0) + + (if val(word_and x MASK16) < val(word_and x (word_not MASK16)) + then 16 else 0) + + (if val(word_and x MASK8) < val(word_and x (word_not MASK8)) + then 8 else 0) + + (if val(word_and x MASK4) < val(word_and x (word_not MASK4)) + then 4 else 0) + + (if val(word_and x MASK2) < val(word_and x (word_not MASK2)) + then 2 else 0) + + (if val(word_and x MASK1) < val(word_and x (word_not MASK1)) + then 1 else 0)) = + word_clz x`;; diff --git a/Examples/bondy.ml b/Examples/bondy.ml new file mode 100644 index 00000000..419d85f7 --- /dev/null +++ b/Examples/bondy.ml @@ -0,0 +1,70 @@ +(* ========================================================================= *) +(* Bondy's theorem (first proof from Bollobas's "Combinatorics", page 4). *) +(* ========================================================================= *) + +let BONDY = prove + (`!(X:A->bool) f n. + 1 <= n /\ X HAS_SIZE n /\ f HAS_SIZE n /\ (!s. s IN f ==> s SUBSET X) + ==> ?x. x IN X /\ {s DIFF {x} | s IN f} HAS_SIZE n`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN + `!m. m <= n - 1 + ==> ?d:A->bool. d HAS_SIZE m /\ d SUBSET X /\ + CARD {s INTER d | s IN f} >= m + 1` + (MP_TAC o SPEC `n - 1`) THEN REWRITE_TAC[GE] THENL + [MATCH_MP_TAC num_INDUCTION THEN CONJ_TAC THENL + [REWRITE_TAC[HAS_SIZE_0; UNWIND_THM2; INTER_EMPTY; EMPTY_SUBSET] THEN + REWRITE_TAC[SIMPLE_IMAGE; IMAGE_CONST; ADD_CLAUSES] THEN + ASM_MESON_TAC[HAS_SIZE; CARD_EQ_0; CARD_SING; LE_REFL]; + ALL_TAC] THEN + X_GEN_TAC `m:num` THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN + ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN + DISCH_THEN(X_CHOOSE_THEN `d:A->bool` STRIP_ASSUME_TAC) THEN + RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN + FIRST_X_ASSUM(DISJ_CASES_TAC o MATCH_MP (ARITH_RULE + `m + 1 <= n ==> SUC m + 1 <= n \/ n = m + 1`)) + THENL + [SUBGOAL_THEN `(d:A->bool) PSUBSET X` MP_TAC THENL + [ASM_MESON_TAC[PSUBSET; ARITH_RULE `SUC m <= n - 1 ==> ~(m = n)`]; + ASM_REWRITE_TAC[PSUBSET_ALT]] THEN + DISCH_THEN(X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC) THEN + EXISTS_TAC `(a:A) INSERT d` THEN + ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; INSERT_SUBSET; FINITE_INSERT] THEN + TRANS_TAC LE_TRANS `CARD {s INTER d:A->bool | s IN f}` THEN + ASM_REWRITE_TAC[] THEN REWRITE_TAC[SIMPLE_IMAGE] THEN + MATCH_MP_TAC CARD_IMAGE_LE2 THEN ASM SET_TAC[]; + ALL_TAC] THEN + MP_TAC(ISPECL [`\s:A->bool. s INTER d`; `f:(A->bool)->bool`] + CARD_IMAGE_EQ_INJ) THEN + ASM_SIMP_TAC[GSYM SIMPLE_IMAGE; LEFT_IMP_EXISTS_THM; NOT_FORALL_THM; + ARITH_RULE `SUC m <= n - 1 ==> ~(m + 1 = n)`] THEN + MAP_EVERY X_GEN_TAC [`t:A->bool`; `u:A->bool`] THEN + REWRITE_TAC[NOT_IMP] THEN STRIP_TAC THEN + SUBGOAL_THEN `?e:A. e IN X /\ ~(e IN t <=> e IN u)` STRIP_ASSUME_TAC THENL + [ASM SET_TAC[]; ALL_TAC] THEN + EXISTS_TAC `(e:A) INSERT d` THEN + ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; INSERT_SUBSET; FINITE_INSERT] THEN + CONJ_TAC THENL [COND_CASES_TAC THEN ASM SET_TAC[]; ALL_TAC] THEN + FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE + `x = m + 1 ==> x < y ==> SUC m + 1 <= y`)) THEN + REWRITE_TAC[SIMPLE_IMAGE] THEN MATCH_MP_TAC CARD_IMAGE_LT2 THEN + ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN + DISCH_THEN(MP_TAC o SPECL [`t:A->bool`; `u:A->bool`]) THEN ASM SET_TAC[]; + ASM_SIMP_TAC[LE_REFL; SUB_ADD] THEN + DISCH_THEN(X_CHOOSE_THEN `d:A->bool` STRIP_ASSUME_TAC) THEN + RULE_ASSUM_TAC(REWRITE_RULE[HAS_SIZE]) THEN + SUBGOAL_THEN `(d:A->bool) PSUBSET X` MP_TAC THENL + [ASM_MESON_TAC[PSUBSET; ARITH_RULE `1 <= n ==> ~(n - 1 = n)`]; + ASM_REWRITE_TAC[PSUBSET_ALT]] THEN + MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:A` THEN STRIP_TAC THEN + SUBGOAL_THEN `d = X DELETE (a:A)` SUBST_ALL_TAC THENL + [ASM_SIMP_TAC[SET_RULE + `a IN X ==> (d = X DELETE a <=> ~(a IN d) /\ a INSERT d = X)`] THEN + MATCH_MP_TAC CARD_SUBSET_EQ THEN + ASM_SIMP_TAC[CARD_CLAUSES; INSERT_SUBSET] THEN ASM_ARITH_TAC; + ASM_SIMP_TAC[HAS_SIZE; SIMPLE_IMAGE; FINITE_IMAGE; GSYM LE_ANTISYM] THEN + CONJ_TAC THENL [ASM_MESON_TAC[CARD_IMAGE_LE]; ALL_TAC] THEN + TRANS_TAC LE_TRANS `CARD {s INTER X DELETE (a:A) | s IN f}` THEN + ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP_LE THEN AP_TERM_TAC THEN + REWRITE_TAC[SIMPLE_IMAGE] THEN MATCH_MP_TAC IMAGE_EQ THEN + ASM SET_TAC[]]]);; diff --git a/Library/words.ml b/Library/words.ml index 8cce2b2e..500b28a0 100644 --- a/Library/words.ml +++ b/Library/words.ml @@ -22,17 +22,26 @@ (* There are conversions like WORD_REDUCE_CONV for reducing via proof *) (* expressions built up from concrete words like `word 255:byte`. *) (* *) -(* Some simple decision procedures for proving basic equalities are here too *) -(* and have limited and somewhat complementary scopes: *) +(* Some simple decision procedures for proving basic word lemmas are here *) +(* too, and have limited and somewhat complementary scopes: *) +(* *) (* - WORD_RULE for simple algebraic properties *) (* - WORD_BITWISE_RULE for bitwise-type properties of logical operations *) (* - WORD_ARITH for things involving numerical values *) (* - WORD_BLAST for fixed-size bitwise expansions followed by arithmetic *) +(* - BITBLAST_RULE is a BDD-based "flattening" or "bit-blasting" rule *) (* *) -(* (c) Copyright, John Harrison 2019-2020 *) +(* (c) Copyright, John Harrison 2019-2024 *) (* (c) Copyright, Mario Carneiro 2020 *) +(* (c) Copyright, June Lee 2022-2024 *) (* ========================================================================= *) +needs "Library/bdd.ml";; + +(* ------------------------------------------------------------------------- *) +(* Some common word sizes. *) +(* ------------------------------------------------------------------------- *) + let HAS_SIZE_8 = HAS_SIZE_DIMINDEX_RULE `:8`;; let HAS_SIZE_16 = HAS_SIZE_DIMINDEX_RULE `:16`;; let HAS_SIZE_32 = HAS_SIZE_DIMINDEX_RULE `:32`;; @@ -7795,6 +7804,315 @@ let WORD_TO_IWORD_CONV = let WORD_IREDUCE_CONV = WORD_REDUCE_CONV THENC ONCE_DEPTH_CONV WORD_TO_IWORD_CONV;; +(* ------------------------------------------------------------------------- *) +(* Expanding a natural number sum in a more "balanced" way. *) +(* ------------------------------------------------------------------------- *) + +let EXPAND_NSUM_BALANCE_CONV = + let op = `(+):num->num->num` in + let dest = dest_binop op + and mk = mk_binop op + and lmk = list_mk_binop op + and PRV = AC ADD_AC in + let rec balance tm = + let tms = striplist dest tm in + let n = length tms in + if n <= 3 then tm else + let tms1,tms2 = chop_list (n / 2) tms in + mk (balance(lmk tms1)) (balance(lmk tms2)) in + fun tm -> + let th = EXPAND_NSUM_CONV tm in + let tm' = rand(concl th) in + let th' = PRV(mk_eq(tm',balance tm')) in + TRANS th th';; + +(* ------------------------------------------------------------------------- *) +(* Convert a natural number expression to the form "val(some_word)" *) +(* ------------------------------------------------------------------------- *) + +let WORDIFY_CONV = + let m_ty = `:M` and n_ty = `:N` and p_ty = `:P` and num_ty = `:num` + and and_th = TAUT `T /\ T <=> T` + and pth_bitval = prove + (`!b. bitval b = val(word(bitval b):1 word)`, + REWRITE_TAC[VAL_WORD_BITVAL]) + and pth_add = prove + (`dimindex(:M) < dimindex(:P) /\ dimindex(:N) < dimindex(:P) + ==> !x y. val(x:M word) + val(y:N word) = + val(word_add (word_zx x) (word_zx y):P word)`, + REPEAT STRIP_TAC THEN REWRITE_TAC[VAL_WORD_ADD; VAL_WORD_ZX_GEN] THEN + CONV_TAC MOD_DOWN_CONV THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_LT THEN + TRANS_TAC LTE_TRANS `2 EXP dimindex(:M) + 2 EXP dimindex(:N)` THEN + SIMP_TAC[LT_ADD2; VAL_BOUND] THEN + TRANS_TAC LE_TRANS `2 EXP SUC(MAX (dimindex(:M)) (dimindex(:N)))` THEN + CONJ_TAC THENL + [REWRITE_TAC[EXP; MULT_2] THEN MATCH_MP_TAC LE_ADD2 THEN CONJ_TAC; + ALL_TAC] THEN + REWRITE_TAC[LE_EXP; ARITH_EQ] THEN ASM_ARITH_TAC) + and pth_mul = prove + (`dimindex(:M) + dimindex(:N) <= dimindex(:P) + ==> !x y. val(x:M word) * val(y:N word) = + val(word_mul (word_zx x) (word_zx y):P word)`, + REPEAT STRIP_TAC THEN REWRITE_TAC[VAL_WORD_MUL; VAL_WORD_ZX_GEN] THEN + CONV_TAC MOD_DOWN_CONV THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_LT THEN + TRANS_TAC LTE_TRANS `2 EXP (dimindex (:M) + dimindex (:N))` THEN + ASM_REWRITE_TAC[LE_EXP; ARITH_EQ] THEN REWRITE_TAC[EXP_ADD] THEN + MATCH_MP_TAC LT_MULT2 THEN REWRITE_TAC[VAL_BOUND]) in + let log2 = + let rec log2 n m i = + if n Int(log2 (abs_num n) num_1 0) in + let rec conv tm = + match tm with + Comb(Const("bitval",_),_) -> + GEN_REWRITE_CONV I [pth_bitval] tm + | Comb(Const("val",_),Comb(Const("word",_),_)) -> + TRY_CONV(RAND_CONV(RAND_CONV conv)) tm + | Comb(Const("val",_),_) -> REFL tm + | Comb(Const("NUMERAL",_),_) -> + let n = max_num num_1 (log2(dest_numeral tm)) in + let th1 = SPEC tm (INST_TYPE [mk_finty n,n_ty] VAL_WORD_EQ) in + let th2 = + (RAND_CONV(RAND_CONV DIMINDEX_CONV THENC NUM_EXP_CONV) THENC + NUM_LT_CONV) (lhand(concl th1)) in + SYM(MP th1 (EQT_ELIM th2)) + | Comb(Comb(Const("+",_),_),_) -> + let eth = BINOP_CONV conv tm in + let mtm = rand(lhand(rand(concl eth))) + and ntm = rand(rand(rand(concl eth))) in + let mty = dest_word_ty(type_of mtm) + and nty = dest_word_ty(type_of ntm) in + let pty = max_num mty nty +/ num_1 in + let th = INST_TYPE + [mk_finty mty,m_ty; mk_finty nty,n_ty; mk_finty pty,p_ty] pth_add in + let ath = (BINOP_CONV (BINOP_CONV DIMINDEX_CONV THENC NUM_LT_CONV)) + (lhand(concl th)) in + TRANS eth (SPECL [mtm; ntm] (MP th (EQT_ELIM (TRANS ath and_th)))) + | Comb(Comb(Const("*",_),_),_) -> + let eth = BINOP_CONV conv tm in + let mtm = rand(lhand(rand(concl eth))) + and ntm = rand(rand(rand(concl eth))) in + let mty = dest_word_ty(type_of mtm) + and nty = dest_word_ty(type_of ntm) in + let pty = mty +/ nty in + let th = INST_TYPE + [mk_finty mty,m_ty; mk_finty nty,n_ty; mk_finty pty,p_ty] pth_mul in + let ath = (BINOP2_CONV (BINOP_CONV DIMINDEX_CONV THENC NUM_ADD_CONV) + DIMINDEX_CONV THENC + NUM_LE_CONV) (lhand(concl th)) in + TRANS eth (SPECL [mtm; ntm] (MP th (EQT_ELIM ath))) + | _ -> failwith "WORDIFY_CONV" in + let fullconv = conv THENC GEN_REWRITE_CONV DEPTH_CONV [WORD_ZX_TRIVIAL] in + fun tm -> if type_of tm = num_ty then fullconv tm + else failwith "WORDIFY_CONV";; + +(* ------------------------------------------------------------------------- *) +(* Adjust word sizes in "val(...)" to be possibly larger *) +(* ------------------------------------------------------------------------- *) + +let VAL_WORD_ADJUST_CONV = + let m_ty = `:M` and n_ty = `:N` + and pth = prove + (`dimindex(:M) <= dimindex(:N) + ==> !x. val(x:M word) = val(word_zx x:N word)`, + SIMP_TAC[VAL_WORD_ZX]) in + fun n tm -> + match tm with + Comb(Const("val",_),_) -> + let m = dest_word_ty(type_of(rand tm)) in + if m =/ n then REFL tm + else if m >/ n then failwith "VAL_WORD_ADJUST_CONV: too small" else + let th = INST_TYPE[mk_finty m,m_ty; mk_finty n,n_ty] pth in + let cth = (BINOP_CONV DIMINDEX_CONV THENC NUM_LE_CONV) + (lhand(concl th)) in + SPEC (rand tm) (MP th (EQT_ELIM cth)) + | _ -> failwith "VAL_WORD_ADJUST_CONV: wrong form of term";; + +let VAL_WORD_ADJUST_BINOP_CONV tm = + let tm1 = lhand tm and tm2 = rand tm in + let n = max_num (dest_word_ty(type_of(rand tm1))) + (dest_word_ty(type_of(rand tm2))) in + BINOP_CONV (VAL_WORD_ADJUST_CONV n) tm;; + +(* ------------------------------------------------------------------------- *) +(* Convert a natural number atom m = n, m < n etc. to word form. *) +(* ------------------------------------------------------------------------- *) + +let WORDIFY_ATOM_CONV = + let num_ty = `:num` + and pth = prove + (`!(x:N word) (y:N word). + val x < val y <=> + (~bit (dimindex(:N)-1) x /\ bit (dimindex(:N)-1) y) \/ + (~bit (dimindex(:N)-1) x \/ bit (dimindex(:N)-1) y) /\ + bit (dimindex(:N)-1) (word_sub x y)`, + CONV_TAC WORD_ARITH) in + let pat = + mk_abs(`x:num`, + subst[`x:num`,`dimindex(:N)-1`] + (rand(snd(strip_forall(concl pth))))) in + let VAL_LT_CONV = + GEN_REWRITE_CONV I [pth] THENC + PAT_CONV pat (LAND_CONV DIMINDEX_CONV THENC NUM_SUB_CONV) in + let conv tm = + match tm with + Comb(Comb(Const("=",_),_),t) when type_of t = num_ty -> + (BINOP_CONV WORDIFY_CONV THENC + VAL_WORD_ADJUST_BINOP_CONV THENC + GEN_REWRITE_CONV I [VAL_EQ]) tm + | Comb(Comb(Const("<",_),_),_) -> + (BINOP_CONV WORDIFY_CONV THENC + VAL_WORD_ADJUST_BINOP_CONV THENC + VAL_LT_CONV) tm + | Comb(Comb(Const(">",_),_),_) -> + (BINOP_CONV WORDIFY_CONV THENC + VAL_WORD_ADJUST_BINOP_CONV THENC + GEN_REWRITE_CONV I [GT] THENC + VAL_LT_CONV) tm + | Comb(Comb(Const("<=",_),_),_) -> + (BINOP_CONV WORDIFY_CONV THENC + VAL_WORD_ADJUST_BINOP_CONV THENC + GEN_REWRITE_CONV I [GSYM NOT_LT] THENC + RAND_CONV VAL_LT_CONV) tm + | Comb(Comb(Const(">=",_),_),_) -> + (BINOP_CONV WORDIFY_CONV THENC + VAL_WORD_ADJUST_BINOP_CONV THENC + GEN_REWRITE_CONV I [GE] THENC + GEN_REWRITE_CONV I [GSYM NOT_LT] THENC + RAND_CONV VAL_LT_CONV) tm + | _ -> failwith "WORDIFY_ATOM_CONV" in + conv;; + +(* ------------------------------------------------------------------------- *) +(* Convert a word(....) term with composite inside to word form. *) +(* ------------------------------------------------------------------------- *) + +let WORDIFY_WORD_CONV = + let conv = + RAND_CONV WORDIFY_CONV THENC + (GEN_REWRITE_CONV I [WORD_VAL] ORELSEC + GEN_REWRITE_CONV I [GSYM word_zx]) in + fun tm -> + match tm with + Comb(Const("word",_),t) when not(is_numeral t) -> conv tm + | _ -> failwith "WORDIFY_WORD_CONV";; + +(* ------------------------------------------------------------------------- *) +(* Expanding multiplication, popcount and unsigned word ordering relations. *) +(* ------------------------------------------------------------------------- *) + +let WORD_MUL_EXPAND_CONV = + let pth = prove + (`!b x:N word. + word(bitval b * val x) = + word_and (word_neg(word(bitval b))) x`, + REPEAT GEN_TAC THEN REWRITE_TAC[WORD_AND_MASK] THEN + COND_CASES_TAC THEN + ASM_REWRITE_TAC[BITVAL_CLAUSES; MULT_CLAUSES; WORD_VAL]) in + let conv = + GEN_REWRITE_CONV I [REWRITE_RULE[NUMSEG_LT_DIMINDEX] WORD_MUL_EXPAND] THENC + RAND_CONV + (LAND_CONV(RAND_CONV(LAND_CONV DIMINDEX_CONV THENC NUM_SUB_CONV)) THENC + EXPAND_NSUM_BALANCE_CONV) THENC + ONCE_DEPTH_CONV BIT_WORD_CONV THENC + GEN_REWRITE_CONV DEPTH_CONV + [BITVAL_CLAUSES; MULT_CLAUSES; ADD_CLAUSES] THENC + GEN_REWRITE_CONV TOP_SWEEP_CONV [WORD_ADD] THENC + GEN_REWRITE_CONV ONCE_DEPTH_CONV [WORD_VAL; pth] + and swap = GEN_REWRITE_CONV I [WORD_MUL_SYM] in + fun tm -> + match tm with + Comb(Comb(Const("word_mul",_),_),Comb(Const("word",_),n)) + when is_numeral n -> (swap THENC conv) tm + | Comb(Comb(Const("word_mul",_),Comb(Const("word",_),n)),_) + when is_numeral n -> conv tm + | Comb(Comb(Const("word_mul",_),x),y) -> conv tm + | _ -> failwith "WORD_MUL_EXPAND_CONV";; + +let WORD_POPCOUNT_EXPAND_CONV = + GEN_REWRITE_CONV I + [REWRITE_RULE[NUMSEG_LT_DIMINDEX] WORD_POPCOUNT_NSUM] THENC + LAND_CONV (RAND_CONV(LAND_CONV DIMINDEX_CONV THENC NUM_SUB_CONV)) THENC + EXPAND_NSUM_BALANCE_CONV;; + +let WORD_URELATION_EXPAND_CONV = + GEN_REWRITE_CONV I + (map (REWRITE_CONV[relational2; word_ule; word_ult; word_uge; word_ugt]) + [`word_ule (x:N word) y`; `word_ult (x:N word) y`; + `word_uge (x:N word) y`; `word_ugt (x:N word) y`]);; + +(* ------------------------------------------------------------------------- *) +(* Basic bit-blasting tactic. *) +(* ------------------------------------------------------------------------- *) + +let BITBLAST_THEN = + let carrying tm = + match tm with + Comb(Comb(Const("word_add",_),_),_) -> true + | Comb(Comb(Const("word_sub",_),_),_) -> true + | Comb(Const("word_neg",_), + Comb(Const("word",_), + Comb(Const("bitval",_),_))) -> false + | Comb(Const("word_neg",_),_) -> true + | _ -> false + and BITWISE_EXPAND_CONV = + GEN_REWRITE_CONV I [WORD_EQ_BITS_ALT] THENC + BINDER_CONV(LAND_CONV(RAND_CONV(!word_SIZE_CONV))) THENC + EXPAND_CASES_CONV in + let BITBLAST_EQUATION th = + let ths = CONJUNCTS(CONV_RULE BITWISE_EXPAND_CONV th) in + end_itlist CONJ (map (CONV_RULE + (LAND_CONV + (BIT_WORD_CONV THENC SUBS_CONV[th] THENC + TOP_DEPTH_CONV (BIT_WORD_CONV o check (not o carrying o rand))) THENC + SYM_CONV THENC + RAND_CONV(REWRITE_CONV[]))) ths) in + let wordbits = + let bit_tm = `bit:num->(N)word->bool` and n_ty = `:N` in + let wordbits_var tm = + try let ty = type_of tm in + let n = dest_word_ty ty in + let btm = inst[mk_finty n,n_ty] bit_tm in + map (fun i -> mk_comb(mk_comb(btm,mk_small_numeral i),tm)) + (0--(Num.int_of_num n-1)) + with Failure _ -> [] in + let rec interleave lis = + match lis with + [] -> [] + | []::rst -> interleave rst + | (h::t)::rst -> h::(interleave(rst @ [t])) in + fun tm -> interleave (map wordbits_var (frees tm)) in + fun tac -> + REPEAT(GEN_TAC ORELSE CONJ_TAC) THEN + REPEAT((COND_CASES_TAC THEN POP_ASSUM MP_TAC) ORELSE + (CHANGED_TAC(CONV_TAC(ONCE_DEPTH_CONV let_CONV)))) THEN + W(fun (_,w) -> let vars = wordbits w in + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN REWRITE_TAC[] THEN + CONV_TAC(DEPTH_CONV(WORD_RED_CONV ORELSEC NUM_RED_CONV)) THEN + CONV_TAC(ONCE_DEPTH_CONV WORD_URELATION_EXPAND_CONV) THEN + GEN_REWRITE_TAC TOP_DEPTH_CONV + [WORD_ODDPARITY_POPCOUNT; WORD_EVENPARITY_POPCOUNT; + WORD_CTZ_EMULATION_POPCOUNT; GSYM WORD_CTZ_REVERSEFIELDS] THEN + CONV_TAC(ONCE_DEPTH_CONV WORD_POPCOUNT_EXPAND_CONV) THEN + CONV_TAC(ONCE_DEPTH_CONV WORDIFY_WORD_CONV) THEN + CONV_TAC(ONCE_DEPTH_CONV WORDIFY_ATOM_CONV) THEN + CONV_TAC(DEPTH_CONV WORD_MUL_EXPAND_CONV) THEN + REPEAT(W(fun (_,w) -> + let t = hd(sort free_in (find_terms carrying w)) in + let v = genvar(type_of t) in + ABBREV_TAC(mk_eq(v,t)))) THEN + CONV_TAC(ONCE_DEPTH_CONV + (BITWISE_EXPAND_CONV THENC TOP_DEPTH_CONV BIT_WORD_CONV)) THEN + CONV_TAC(TOP_DEPTH_CONV + (BIT_WORD_CONV o check (not o carrying o rand))) THEN + TRY(POP_ASSUM_LIST + (MP_TAC o end_itlist CONJ o map BITBLAST_EQUATION o rev)) THEN + REWRITE_TAC[] THEN tac vars);; + +let BITBLAST_TAC = BITBLAST_THEN (CONV_TAC o BDD_DEFTAUT);; + +let BITBLAST_RULE tm = time prove(tm,BITBLAST_TAC);; + (* ------------------------------------------------------------------------- *) (* SIMD repetition of a unary (usimd) or binary (simd) function. *) (* ------------------------------------------------------------------------- *) diff --git a/holtest b/holtest index 548d48cd..45a7704b 100755 --- a/holtest +++ b/holtest @@ -35,8 +35,10 @@ echo '### Loading Library/bdd.ml, Examples/bdd_examples.ml'; (echo 'loadt "Library/bdd.ml";;'; echo 'loadt "Examples/bdd_examples.ml";;') | (time $hollight) echo '### Loading Library/binary.ml'; echo 'loadt "Library/binary.ml";;' | (time $hollight) echo '### Loading Library/binomial.ml'; echo 'loadt "Library/binomial.ml";;' | (time $hollight) +echo '### Loading Examples/bitblast.ml'; echo 'loadt "Examples/bitblast.ml";;' | (time $hollight) echo '### Loading Library/bitmatch.ml'; echo 'loadt "Library/bitmatch.ml";;' | (time $hollight) echo '### Loading Library/bitsize.ml'; echo 'loadt "Library/bitsize.ml";;' | (time $hollight) +echo '### Loading Examples/bondy.ml'; echo 'loadt "Examples/bondy.ml";;' | (time $hollight) echo '### Loading Examples/borsuk.ml'; echo 'loadt "Examples/borsuk.ml";;' | (time $hollight) echo '### Loading Examples/brunn_minkowski.ml'; echo 'loadt "Examples/brunn_minkowski.ml";;' | (time $hollight) echo '### Loading Library/card.ml'; echo 'loadt "Library/card.ml";;' | (time $hollight) diff --git a/holtest.mk b/holtest.mk index 12a5f200..55dd194e 100644 --- a/holtest.mk +++ b/holtest.mk @@ -6,8 +6,10 @@ STANDALONE_EXAMPLES:=\ Examples/bdd_examples \ Library/binary \ Library/binomial \ + Examples/bitblast \ Library/bitmatch \ Library/bitsize \ + Examples/bondy \ Examples/borsuk \ Examples/brunn_minkowski \ Library/card \ diff --git a/lib.ml b/lib.ml index 11a17126..0ac24fc7 100755 --- a/lib.ml +++ b/lib.ml @@ -840,18 +840,19 @@ let num_of_string = (* ------------------------------------------------------------------------- *) let strings_of_file filename = - let fd = try Pervasives.open_in filename - with Sys_error _ -> - failwith("strings_of_file: can't open "^filename) in + let fd = + try open_in filename + with Sys_error _ -> failwith("strings_of_file: can't open "^filename) in let rec suck_lines acc = - try let l = Pervasives.input_line fd in - suck_lines (l::acc) - with End_of_file -> rev acc in + let l = try [input_line fd] with End_of_file -> [] in + if l = [] then rev acc else suck_lines(hd l::acc) in let data = suck_lines [] in - (Pervasives.close_in fd; data);; + (close_in fd; data);; let string_of_file filename = - end_itlist (fun s t -> s^"\n"^t) (strings_of_file filename);; + let fd = open_in_bin filename in + let data = really_input_string fd (in_channel_length fd) in + (close_in fd; data);; let file_of_string filename s = let fd = Pervasives.open_out filename in