Work on hackers-deligh & queens examples.

Add int.NumOf realization.

Makefile.in

@@ -840,7 +840,7 @@ ifeq (@enable_coq_support@,yes)
 
 ifeq (@enable_coq_libs@,yes)
 
-COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
+COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power NumOf
 COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES)
 COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
 

examples/hackers-delight.mlw

@@ -2,9 +2,12 @@
 
     *second edition *)
 
-module Hackers_delight
-  use import int.Int
-  use import bool.Bool
+(** {2 Utilitaries}
+    We introduce in this theory two functions that will help us
+    write properties on bit-manipulating procedures *)
+
+theory Utils
+
   use import bv.BV32
 
   constant one : t = of_int 1
@@ -14,19 +17,8 @@ module Hackers_delight
   function max (x y : t) : t = (if ult x y then y else x)
   function min (x y : t) : t = (if ult x y then x else y)
 
-  (** {2 ASCII cheksum }
-    In the beginning the encoding of an ascii character was done on 8
-    bits: the first 7 bits were used for the carracter itself while
-    the 8th bit was used as a cheksum: a mean to detect errors. The
-    cheksum value was the binary sum of the 7 other bits, allowing the
-    detections of any change of an odd number of bits in the initial
-    value. Let's prove it! *)
-
-  (** {6 Hamming distance } *)
-
-  (** In order to express these properties we start by introducing a
-      function that returns the number of 1-bit in a bitvector (p.82)
-      *)
+  (** We start by introducing a function that returns the number of
+      1-bit in a bitvector (p.82) *)
 
   function count (bv : t) : t =
     let x = sub bv (bw_and (lsr_bv bv one) (of_int 0x55555555)) in
@@ -38,12 +30,34 @@ module Hackers_delight
     let x = add x (lsr_bv x (of_int 16)) in
     bw_and x (of_int 0x0000003F)
 
-  (** We can verify our definition by, first, checking that there are no
-      1-bits in the bitvector "zero": *)
+  (** We then define the associated notion of distance, namely
+      "Hamming distance", that counts the number of bits that differ
+      between two bitvectors. *)
+
+  function hammingD (a b : t) : t = count (bw_xor a b)
+
+end
+
+(** {2 Correctness of Utils}
+    Before using our two functions let's first check that they are correct !
+*)
+
+module Utils_Spec
+  use import int.Int
+  use import int.NumOf
+  use import bv.BV32
+  use import Utils
+
+  (** {6 count correctness } *)
+
+  (** Let's start by checking that there are no 1-bits in the
+      bitvector "zero": *)
 
   lemma countZero: count zero = zero
 
-  (** And then, for b a bitvector with n 1-bits, checking that if its
+  lemma numOfZero: NumOf.numof (\i. nth zero i) 0 32 = 0
+
+  (** Now, for b a bitvector with n 1-bits, we check that if its
       first bit is 0 then shifting b by one on the right doesn't
       change the number of 1-bit. And if its first bit is one, then
       there are n-1 1-bits in the shifting of b by one on the right. *)
@@ -52,18 +66,6 @@ module Hackers_delight
     (not (nth_bv b zero) <-> count (lsr_bv b one) = count b) /\
     (nth_bv b zero <-> count (lsr_bv b one) = sub (count b) one)
 
-  use import int.NumOf
-
-  lemma tointzero: to_uint zero = 0
-  lemma tointone: to_uint one = 1
-
-  lemma numOfZero: NumOf.numof (\i. nth zero i) 0 32 = 0
-
-  lemma numof_change_equiv:
-    forall p1 p2: int -> bool, a b: int.
-    (forall j: int. a <= j < b -> p1 j <-> p2 j) ->
-    numof p2 a b = numof p1 a b
-
   let rec lemma numof_shift (p q : int -> bool) (a b k: int) : unit
     requires {forall i. q i = p (i + k)}
     variant {b - a}
@@ -72,15 +74,14 @@ module Hackers_delight
     if a < b then
     numof_shift p q a (b-1) k
 
-
-  let rec lemma countAux (bv : t) : unit
+  let rec lemma countSpec_Aux (bv : t) : unit
   variant {bv with ult}
   ensures {to_uint (count bv) = NumOf.numof (nth bv) 0 32}
   =
     if bv = zero then ()
     else
     begin
-      countAux (lsr_bv bv one);
+      countSpec_Aux (lsr_bv bv one);
       assert {
                  let x = (if nth_bv bv zero then 1 else 0) in
                   let f = nth bv in
@@ -93,32 +94,33 @@ module Hackers_delight
            }
     end
 
+  (** With these lemmas, we can now prove the correctness property of
+  count: *)
+
   lemma countSpec: forall b. to_uint (count b) = NumOf.numof
         (nth b) 0 32
 
-  (** We then define the associated notion of distance, namely
-      "Hamming distance", that counts the number of bits that differ
-      between two bitvectors. *)
-
-  function hammingD (a b : t) : t = count (bw_xor a b)
-
-  predicate nth_diff (a b : t) (i : int) = nth a i <> nth b i
+  (** {6 hammingD correctness } *)
 
   use HighOrd as HO
 
-  function fun_or (f g : HO.pred 'a) : HO.pred 'a = \x. f x \/ g x
+  predicate nth_diff (a b : t) (i : int) = nth a i <> nth b i
 
+  (** The correctness property can be express as the following: *)
   let lemma hamming_spec (a b : t) : unit
   ensures {to_uint (hammingD a b) = NumOf.numof (nth_diff a b) 0 32}
   =
    assert { forall i. 0 <= i < 32 -> nth (bw_xor a b) i <-> (nth_diff a b i) }
 
-  (** It is indeed a distance in the algebraic sense: *)
+  (** In addition we can prove that it is indeed a distance in the
+      algebraic sens: *)
 
   lemma symmetric: forall a b. hammingD a b = hammingD b a
 
   lemma separation: forall a b. hammingD a b = zero <-> a = b
 
+  function fun_or (f g : HO.pred 'a) : HO.pred 'a = \x. f x \/ g x
+
   let rec lemma numof_or (p q : int -> bool) (a b: int) : unit
     variant {b - a}
     ensures {numof (fun_or p q) a b <= numof p a b + numof q a b}
@@ -133,16 +135,32 @@ module Hackers_delight
     numof (fun_or (nth_diff a b) (nth_diff b c)) 0 32 >=
     numof (nth_diff a c) 0 32}
 
-  lemma triangleInequality: forall a b c. (* not proved ! :-( *)
+  lemma triangleInequality: forall a b c.
     uge (add (hammingD a b) (hammingD b c)) (hammingD a c)
 
+end
+
+module Hackers_delight
+  use import int.Int
+  use import int.NumOf
+  use import bool.Bool
+  use import bv.BV32
+  use import Utils
+
+  (** {2 ASCII cheksum }
+    In the beginning the encoding of an ascii character was done on 8
+    bits: the first 7 bits were used for the carracter itself while
+    the 8th bit was used as a cheksum: a mean to detect errors. The
+    cheksum value was the binary sum of the 7 other bits, allowing the
+    detections of any change of an odd number of bits in the initial
+    value. Let's prove it! *)
 
   (** {6 Checksum computation and correctness } *)
 
   (** A ascii character is valid if its number of bits is even.
       (Remember that a binary number is odd if and only if its first
       bit is 1) *)
-  predicate validAscii (b : t) = not (nth_bv (count b) zero)
+  predicate validAscii (b : t) = (nth_bv (count b) zero) = False
 
   (** The ascii checksum aim is to make any character valid in the
       sens that we just defined. One way to implement it is to count

lib/coq/bv/BV_Gen.v

@@ -1500,4 +1500,3 @@ Lemma two_power_size_val : ((max_int + 1%Z)%Z = (bv.Pow2int.pow2 size_int)).
   unfold max_int.
   omega.
 Qed.
-

theories/bv.why

@@ -98,7 +98,7 @@ theory Pow2int
 
 end
 
-(** {2 Generic theory of bitvectors (arbitrary length)} *)
+(** {2 Generic theory of Bit Vectors (arbitrary length)} *)
 
 theory BV_Gen
 
@@ -110,6 +110,8 @@ theory BV_Gen
 
   type t
 
+  (** [nth b n] is the n-th bit of x (0 <= n < size). bit 0 is
+      the least significant bit *)
   function nth t int : bool
 
   constant zero : t
@@ -123,7 +125,9 @@ theory BV_Gen
   predicate eq (v1 v2 : t) =
     forall n. 0 <= n < size_int -> nth v1 n = nth v2 n
 
-  axiom Extensionality: forall x y : t. eq x y -> x = y
+  axiom Extensionality: forall x y : t [eq x y]. eq x y -> x = y
+
+  (** Bitwise operators *)
 
   function bw_and (v1 v2 : t) : t
   axiom Nth_bw_and:
@@ -212,24 +216,18 @@ theory BV_Gen
   predicate uge (x y : t) =
     Int.(>=) (to_uint x) (to_uint y)
 
-  (** binary predicate for signed less than *)
   predicate slt (v1 v2 : t) =
     Int.(<) (to_int v1) (to_int v2)
 
-  (** binary predicate for signed less than or equal *)
   predicate sle (v1 v2 : t) =
     Int.(<=) (to_int v1) (to_int v2)
 
-  (**  binary predicate for signed greater than *)
   predicate sgt (v1 v2 : t) =
     Int.(>) (to_int v1) (to_int v2)
 
-  (**  binary predicate for signed greater than or equal *)
   predicate sge (v1 v2 : t) =
     Int.(>=) (to_int v1) (to_int v2)
 
-  (** [nth(_bv) b n] is the n-th bit of x (0 <= n < size). bit 0 is
-      the least significant bit *)
   function nth_bv t t: bool
 
   axiom Nth_bv_is_nth:
@@ -242,40 +240,34 @@ theory BV_Gen
   axiom Of_int_ones:
     ones = of_int max_int
 
-  (** addition modulo 2^m *)
+  (** Arithmetic operators *)
+
   function add (v1 v2 : t) : t
   axiom to_uint_add:
     forall v1 v2. to_uint (add v1 v2) =  mod (Int.(+) (to_uint v1) (to_uint v2)) two_power_size
 
-  (** 2's complement subtraction modulo 2^m *)
   function sub (v1 v2 : t) : t
   axiom to_uint_sub:
     forall v1 v2. to_uint (sub v1 v2) = mod (Int.(-) (to_uint v1) (to_uint v2)) two_power_size
 
-  (** 2's complement unary minus *)
   function neg (v1 : t) : t
   axiom to_uint_neg:
     forall v. to_uint (neg v) = mod (Int.(-_) (to_uint v)) two_power_size
 
-  (** multiplication modulo 2^m *)
   function mul (v1 v2 : t) : t
   axiom to_uint_mul:
     forall v1 v2. to_uint (mul v1 v2) = mod (Int.( * ) (to_uint v1) (to_uint v2)) two_power_size
 
-  (** unsigned division, truncating towards 0 (undefined if divisor is 0) *)
   function udiv (v1 v2 : t) : t
   axiom to_uint_udiv:
     forall v1 v2. to_uint (udiv v1 v2) = div (to_uint v1) (to_uint v2)
 
-  (** unsigned remainder from truncating division (undefined if divisor is 0) *)
   function urem (v1 v2 : t) : t
   axiom to_uint_urem:
     forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
 
-  (** rotate right  *)
   function rotate_right (v n : t) : t
 
-  (** rotate left  *)
   function rotate_left (v n : t) : t
 
   axiom Nth_rotate_left :
@@ -286,9 +278,6 @@ theory BV_Gen
     forall v n i. ult i size -> ult n (sub ones size) ->
       nth_bv (rotate_right v n) i = nth_bv v (urem (add i n) size)
 
-  (** The guard on n for the rotation is not necessary if size is a
-  power of two. *)
-
   (** logical shift right *)
   function lsr_bv t t : t
 

theories/int.why

@@ -332,6 +332,11 @@ theory NumOf
     not (p1 i) -> p2 i ->
     numof p2 a b > numof p1 a b
 
+  lemma numof_change_equiv:
+    forall p1 p2: int -> bool, a b: int.
+    (forall j: int. a <= j < b -> p1 j <-> p2 j) ->
+    numof p2 a b = numof p1 a b
+
 end
 
 (** {2 Sum} *)