Library listbit_correct

Require Import Max.
Require Import ssreflect ssrnat ssrbool ssrfun eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import listbit.
Import ListBit.

This file provides functions to interpret lists of bits as (signed or unsigned) integers and proves their arithmetic properties.

This is for the implementation of finite-size integers.

Local Open Scope listbit_scope.
Local Open Scope zarith_ext_scope.

interpretation of listbits as unsigned integers, and properties

Fixpoint ulst2Z l : Z :=
  match l with
    | nil => 0
    | hd :: tl =>
      match hd with
        | i => 2 ^^ length tl + ulst2Z tl
        | o => ulst2Z tl
      end
  end.

Notation "'[[' l ']]u'" := (ulst2Z l) (at level 30) : listbit_correct_scope.

Open Local Scope listbit_correct_scope.

Lemma ulst2Z_o : forall l, [[ o :: l ]]u = [[ l ]]u.

Lemma ulst2Z_i : forall l, [[ i :: l ]]u = 2 ^^ length l + [[ l ]]u.

Lemma ulst2Z_zeros : forall n, [[ zeros n ]]u = 0.

Lemma ulst2Z_ones : forall n, [[ ones n ]]u = Zpower 2 n - 1.

Lemma ulst2Z_app : forall l l', [[ l ++ l' ]]u = [[ l ++ zeros (length l') ]]u + ulst2Z l'.

Lemma ulst2Z_app_zeros : forall l n, [[ l ++ zeros n ]]u = [[ l ]]u * 2 ^^ n.

Lemma ulst2Z_Zpower_inv : forall n a, length a = S n ->
  [[ a ]]u = 2 ^^ n -> a = true :: zeros n.

Lemma Zodd_lst_i : forall lst, Zodd ([[ lst ++ i :: nil ]]u).

Lemma Zeven_lst_o : forall lst, Zeven ([[ lst ++ o :: nil ]]u).

Lemma max_ulst2Z : forall n l, (length l <= n)%coq_nat -> [[ l ]]u < 2 ^^ n.

Lemma min_ulst2Z : forall l, 0 <= [[ l ]]u.

Lemma overflow_length : forall l n, 2 ^^ n <= [[ l ]]u -> (n <= length l)%coq_nat.

Lemma ulst2Z_inj : forall n (v w : list bool),
  length v = n -> length w = n -> [[ v ]]u = [[ w ]]u -> v = w.

Lemma ulst2Z_zeros_inv : forall n l, length l = n -> [[ l ]]u = 0 -> l = zeros n.

Lemma ulst2Z_power : forall n l m,
  (m <= n)%coq_nat -> length l = n -> [[ l ]]u < 2 ^^ m ->
  exists l', l = zeros (n - m) ++ l'.

Lemma ulst2Z_last : forall l b, [[ l ++ b :: nil ]]u = 2 * [[ l ]]u + [[ b :: nil ]]u.

Lemma ulst2Z_erase_leading_zeros: forall l, [[ erase_leading_zeros l ]]u = [[ l ]]u.

correctness of z_extend_lst

Lemma zext_lst_correct : forall p l, [[ zext_lst p l ]]u = [[ l ]]u.

Z2ulst

NB: positive is a type that represents strictly positive number xH is the leading 1 xO (resp. xH) represents the bit 0 (resp. 1) binary numbers are represented in signed-magnitude notation, with the LSB first

Fixpoint pos2lst p :=
  match p with
    | xI p' => i :: pos2lst p'
    | xO p' => o :: pos2lst p'
    | xH => i :: nil
  end.

Lemma pos2lst_inj : forall p q, pos2lst p = pos2lst q -> p = q.

Lemma pos2lst_len_pos : forall p, (O < length (pos2lst p))%coq_nat.

Lemma pos2lst_O : forall p, ~ pos2lst p = zeros (length (pos2lst p)).

Lemma pos2lst_nil : forall p, pos2lst p <> nil.

Lemma pos2lst_len : forall p m, Zpos p < 2 ^^ m -> (length (pos2lst p) <= m)%coq_nat.

Lemma pos2lst_len2 : forall p m, 2 ^^ m <= Zpos p -> (m < length (pos2lst p))%coq_nat.

Lemma Zpos_Zpower : forall m p, Zpos p = 2 ^^ m -> rev (pos2lst p) = i :: zeros m.

Lemma Zneg_Zpower : forall m p, Zneg p = - 2 ^^ m -> rev (pos2lst p) = i :: zeros m.

Lemma Zpos_Zpower_m1 : forall m p, Zpos p = 2 ^^ m - 1 -> rev (pos2lst p) = ones m.

Definition Z2ulst n :=
  match n with
    | Z0 => nil
    | Zpos p => let l := pos2lst p in rev l
    | _ => nil
  end.

Lemma Z2ulst_2 : forall z, 0 <= z -> Z2ulst (2 * z + 1) = Z2ulst z ++ (true :: nil ).

Lemma Z2ulst_2_0 : forall z, 0 < z -> Z2ulst (2 * z) = Z2ulst z ++ (false :: nil ).

Lemma Z2ulst_2_Zpower : forall k, Z2ulst (2 ^^ k) = true :: zeros k.

Lemma Z2ulst_2_Zpower_m1 : forall k, Z2ulst (2 ^^ k - 1) = ones k.

Lemma Z2ulst_nil : forall z, 0 <= z -> Z2ulst z = nil -> z = 0.

Lemma Z2ulst_inj : forall a b, 0 <= a -> 0 <= b -> Z2ulst a = Z2ulst b -> a = b.

Lemma ulst2Z_rev_poslst: forall p, [[ rev (pos2lst p) ]]u = Zpos p.

Lemma ulst2Z2ulst : forall n, 0 <= n -> [[ Z2ulst n ]]u = n.

Lemma Z2ulst_length : forall z m, z < 2 ^^ m ->
  (length (Z2ulst z) <= m)%coq_nat.

Lemma len_Z2ulst_ulst2Z : forall n l, length l = n ->
  head l = Some true -> length (Z2ulst (ulst2Z l)) = n.

Lemma ulst2Z_not_zeros : forall l, l <> zeros (length l) -> 0 < ulst2Z l.

Lemma Z2ulst_ulst2Z : forall n (l : list bool) (Hlst : length l = n),
  Z2ulst (ulst2Z l) = erase_leading_zeros l.

correctness of comparisons

Lemma listbit_lt_correct : forall n a b, length a = n -> length b = n ->
  listbit_lt a b = true -> [[ a ]]u < [[ b ]]u.

Lemma listbit_lt_correct_alt : forall n m a b, length a = n -> length b = m ->
  forall p, p = max n m ->
    listbit_lt (zext_lst (p - n)%coq_nat a) (zext_lst (p - m)%coq_nat b) = true ->
    [[ zext_lst (p - n)%coq_nat a ]]u < [[ zext_lst (p - m)%coq_nat b ]]u.

Definition pos_lt (a b:positive) : bool :=
  let a' := rev (pos2lst a) in
  let b' := rev (pos2lst b) in
  let max_len := max (length a') (length b') in
  let a'' := zext_lst (max_len - length a') a' in
  let b'' := zext_lst (max_len - length b') b' in
  listbit_lt a'' b''.

Lemma pos_lt_correct' : forall p q, pos_lt p q = true -> Zpos p < Zpos q.

Lemma listbit_lt_correct' : forall n a b, length a = n -> length b = n ->
  [[ a ]]u < [[ b ]]u -> listbit_lt a b = true.

properties of add_lst'/add_lst w.r.t. ulst2Z

Lemma add_lst'_nat : forall n a b carry, length a = n -> length b = n ->
  [[ rev a ]]u + [[ rev b ]]u + [[ carry :: nil ]]u < 2^^n ->
  [[ rev (add_lst' a b carry) ]]u =
  [[ rev a ]]u + [[ rev b ]]u + [[ carry :: nil ]]u.

The hardware addition behaves like the mathematical addition only when non-overflow conditions are met:

Lemma add_lst_nat : forall n a b, length a = n -> length b = n ->
  [[ a ]]u + [[ b ]]u < 2 ^^ n ->
  [[ add_lst a b o ]]u = [[ a ]]u + [[ b ]]u.

Lemma ulst2Z_add_lst' : forall n l k carry,
  length l = n -> length k = n ->
  [[ rev (add_lst' (l++(o ::nil )) (k++(o ::nil )) carry) ]]u =
  [[ rev l ]]u + [[ rev k ]]u + [[ carry::nil ]]u.

Lemma ulst2Z_add_lst : forall n l k carry,
  length l = n -> length k = n ->
  [[ add_lst (o :: l) (o :: k) carry ]]u =
  [[ l ]]u + [[ k ]]u + [[ carry::nil ]]u.

Lemma add_lst'_nat_overflow : forall n (a b : list bool) carry,
  length a = n -> length b = n ->
  2 ^^ n <= [[ rev a ]]u + [[ rev b ]]u + [[ carry :: nil ]]u ->
  [[ rev (add_lst' a b carry) ]]u + 2 ^^ n =
  [[ rev a ]]u + [[ rev b ]]u + [[ carry :: nil ]]u.

Lemma add_lst_nat_overflow : forall n a b,
  length a = n -> length b = n ->
  2 ^^ n <= [[ a ]]u + [[ b ]]u ->
  [[ add_lst a b o ]]u + 2^^n = [[ a ]]u + [[ b ]]u.

subtraction

Lemma sub_lst'_nat : forall n (a b : list bool) borrow,
  length a = n -> length b = n ->
  (0 < n)%coq_nat ->
  [[ a ]]u >= [[ b ]]u + [[ borrow :: nil ]]u ->
  [[ rev (sub_lst' (rev a) (rev b) borrow) ]]u + [[ borrow :: nil ]]u + [[ b ]]u = [[ a ]]u.

Lemma sub_lst_nat : forall n a b borrow,
  length a = n -> length b = n ->
  (0 < n)%coq_nat ->
  [[ a ]]u >= [[ b ]]u + [[ borrow :: nil ]]u ->
  [[ sub_lst a b borrow ]]u + [[ borrow :: nil ]]u + [[ b ]]u = [[ a ]]u.

Lemma sub_lst'_nat_overflow : forall n (a b:list bool) borrow,
  length a = n -> length b = n ->
  (0 < n)%coq_nat ->
  [[ a ]]u < [[ b ]]u + [[ borrow :: nil ]]u ->
  [[ rev (sub_lst' (rev a) (rev b) borrow) ]]u + [[ borrow :: nil ]]u = [[ a ]]u + 2^^n - [[ b ]]u.

Lemma sub_lst_nat_overflow : forall n a b borrow,
  length a = n -> length b = n ->
  (0 < n)%coq_nat ->
  [[ a ]]u < [[ b ]]u + [[ borrow :: nil ]]u ->
  [[ sub_lst a b borrow ]]u + [[ borrow :: nil ]]u = [[ a ]]u + 2^^n - [[ b ]]u.

correctness of adjust

Lemma adjust_ulst2Z: forall n lst, [[ lst ]]u < 2 ^^ n ->
  [[ adjust_ulist lst n ]]u = [[ lst ]]u.

Lemma skipn_Zmod : forall m lst n, (n <= m)%coq_nat -> length lst = m ->
  [[ skipn n lst ]]u = [[lst]]u mod 2 ^^ (m - n).

Lemma adjust_ulst2Z_overflow : forall n lst, 2 ^^ n <= [[ lst ]]u ->
  [[ adjust_ulist lst n ]]u = [[ lst ]]u mod 2 ^^ n.

Lemma zext_lst_Z2ulst : forall n m m', n < 2 ^^ m ->
  zext_lst m' (adjust_ulist (Z2ulst n) (S m)) = adjust_ulist (Z2ulst n) (S (m + m')).

properties of cplt2_lst w.r.t. ulst2Z

Lemma ulst2Z_cplt2_lst_O : forall a, length a = O -> a <> zeros O ->
  [[ cplt2_lst a ]]u = 2 ^^ O - [[ a ]]u.

Lemma ulst2Z_cplt2_lst_1 : forall a, length a = S O -> a <> zeros 1 ->
  [[ cplt2_lst a ]]u = 2 ^^ 1 - [[ a ]]u.

Lemma ulst2Z_cplt2_lst' : forall n a,
  length a = S (S n) -> a <> zeros (S (S n)) ->
  [[ cplt2_lst a ]]u = 2 ^^ (S (S n)) - [[ a ]]u.

Lemma ulst2Z_cplt2_lst : forall n l, length l = n -> l <> zeros n ->
  [[ cplt2_lst l ]]u = 2 ^^ n - [[ l ]]u.

correctness of 2k-multiplication (given k-long inputs, the result fits in 2k)

Lemma umul_lst_nat: forall n l k,length l = S n -> length k = S n ->
[[ umul_lst l k ]]u = [[ l ]]u * [[ k ]]u.

correctness of k-multiplication (given k-long inputs, returns a result in k)

Lemma mul_lst_nat : forall n a b, length a = n -> length b = n ->
[[ a ]]u * [[ b ]]u < 2 ^^ n ->
[[ adjust_ulist (umul_lst a b) n ]]u = [[ a ]]u * [[ b ]]u.

properties of shift-left w.r.t. ulst2Z

Lemma shl_lst_ulst2Z : forall k n (lst : list bool), length lst = n ->
  forall k', (k + k' <= n)%coq_nat ->
    [[ lst ]]u < 2 ^^ k' ->
    [[ shl_lst k lst ]]u = [[ lst ]]u * 2 ^^ k.

Lemma shl_lst_ulst2Z_overflow : forall l a k, l = length a ->
  (k < l)%coq_nat ->
  [[shl_lst k a]]u = ([[a]]u * 2 ^^ k) mod 2 ^^ l.

Lemma shl_ulst2Z' : forall n lst, length lst = n ->
  forall l, ulst2Z lst < 2 ^^ l ->
    forall k, (k + l <= n)%coq_nat ->
      ulst2Z (shl_lst k lst) <= 2 ^^ (l + k) - 2 ^^ k.

properties of shift-left-extend w.r.t. lst2nat

Lemma shl_extend_ulst2Z : forall k n lst, length lst = n ->
  [[ shl_extend_lst k lst ]]u = [[ lst ]]u * 2 ^^ k.

Lemma shl_extend_ulst2Z' : forall n lst, length lst = n ->
  forall l, [[ lst ]]u < 2^^l ->
    forall k, [[ shl_extend_lst k lst ]]u <= 2^^(l+k) - 2^^k.

properties of shrl_lst / ulst2Z

Lemma shrl_lst_shl_lst : forall n l, length l = n ->
  forall m, ulst2Z l < 2 ^^ m ->
    shrl_lst (n - m) (shl_lst (n - m) l) = l.

Lemma listbit_lt_shrl_lst_overflow : forall k n lst, length lst = n -> (k < n)%coq_nat ->
  listbit_lt lst (adjust_ulist (Z2ulst (2 ^^ k)) n) ->
  shrl_lst k lst = zeros n.

properties of s_extend w.r.t. ulst2Z/Z2ulst

Lemma sext_ulst2Z : forall n lst l, length lst = l ->
  0 <= [[ lst ]]u < 2 ^^ (predn l) ->
  [[ sext_lst n lst ]]u = [[ lst ]]u.

Lemma sext_lst_o : forall l n, [[ sext_lst n (o :: l) ]]u = [[ l ]]u.

Lemma sext_lst_i : forall n l,
  [[ sext_lst n (i :: l) ]]u = 2 ^^ (length l) * (2 ^^ (S n) - 1) + [[ l ]]u.

Lemma sext_lst_Z2ulst: forall n m m',
  n < 2 ^^ m ->
  sext_lst m' (adjust_ulist (Z2ulst n) (S m)) =
  adjust_ulist (Z2ulst n) (S (m + m')).

interpretation of list bools as signed integers in 2cplt notation

Definition slst2Z (l : list bool) : Z :=
  match l with
    | nil => 0
    | o :: tl => [[ tl ]]u
    | i :: tl => - 2 ^^ (length tl) + [[ tl ]]u
  end.

Notation "'[[' lst ']]s'" := (slst2Z lst) (at level 30) : listbit_correct_scope.

Lemma slst2Z_o : forall l, [[ o :: l ]]s = [[ l ]]u.

Lemma slst2Z_i : forall l, [[ i :: l ]]s = - 2 ^^ (length l) + [[ l ]]u.

Lemma slst2Z_inj : forall n (a b: list bool), length a = n -> length b = n ->
  [[ a ]]s = [[ b ]]s -> a = b.

Lemma slst2Z_ulst2Z_pos : forall n l, length l = n -> 0 <= [[ l ]]s ->
  [[ l ]]s = [[ l ]]u.

Lemma slst2Z_ulst2Z_pos_equiv : forall n lst, length lst = n ->
  (0 <= [[ lst ]]s <-> [[ lst ]]u < 2 ^^ predn n).

Lemma slst2Z_ulst2Z_neg : forall n l, length l = n -> [[ l ]]s < 0 ->
  [[ l ]]s = [[ l ]]u - 2 ^^ n.

Lemma slst2Z_zeros : forall n, [[ zeros n ]]s = 0.

Lemma max_slst2Z : forall n lst, length lst = S n -> [[ lst ]]s < 2 ^^ n.

Lemma min_slst2Z : forall n l, length l = S n -> - 2 ^^ n <= [[ l ]]s.

Lemma slst2Z_app : forall l e, (O < length l)%coq_nat ->
  [[ l ++ (e :: nil ) ]]s = 2 * [[ l ]]s + [[ e :: nil ]]u.

Lemma slst2Z_Zpower_inv : forall n a, length a = S n ->
  [[ a ]]s = - 2 ^^ n -> a = true :: zeros n.

Lemma bZsgn_Zsgn_slst2Z : forall def n a, length a = n -> a <> zeros n ->
  bZsgn ([[ hd def a :: nil ]]u ) = Zsgn ([[a ]]s).

Lemma slst2Z_neg_ones : forall n lst, length lst = n ->
  forall l', (l' < n)%coq_nat ->
    - 2 ^^ l' <= [[ lst ]]s < 0 ->
    exists lst', lst = ones (n - l') ++ lst'.

Lemma slst2Z_ulst2Z_pos_zeros : forall n lst, length lst = n ->
  forall l', (l' < n)%coq_nat ->
    0 <= [[ lst ]]s < 2^^l' ->
    exists lst', lst = zeros (n - l') ++ lst'.

Lemma slst2Z_shl_lst : forall l lst, length lst = l ->
  forall k l', (l' > k)%coq_nat ->
    forall lst', lst = ones l' ++ lst' \/ lst = zeros l' ++ lst' ->
      [[ shl_lst k lst ]]s = [[ lst ]]s * 2^^k.

Lemma shra_lst_ones : forall n a m, length a = S n ->
  [[ a ]]s < 0 -> (n < m)%coq_nat ->
  shra_lst m a = ones (S n).

Lemma shra_lst_zeros : forall n a m, length a = S n ->
  0 <= [[ a ]]s -> (n < m)%coq_nat ->
  shra_lst m a = zeros (S n).

correctness of cplt2_lst

Lemma cplt2_lst_correct : forall n a, length a = S n -> a <> i :: zeros n ->
[[ cplt2_lst a ]]s = - [[ a ]]s.

from Coq integers to integers in two's complement notation

Definition Z2slst (z : Z) : list bool :=
  match z with
    | Z0 => o :: o :: nil
    | Zpos p => o :: Z2ulst z
    | Zneg p => cplt2_lst (o :: Z2ulst (Zpos p))
  end.

Lemma Z2slst2Z : forall z, [[ Z2slst z ]]s = z.

Lemma Z2slst_weird : forall m, Z2slst (- 2 ^^ m) = i :: i :: zeros m.

Lemma Z2slst_weird_len : forall n, length (Z2slst (- 2 ^^ n)) = n.+2.

Lemma Z2slst_max_len : forall n, length (Z2slst (2 ^^ n)) = n.+2.

Lemma Z2slst_len1 : forall z n, 2 ^^ n <= z -> (n < length (Z2slst z))%coq_nat.

Lemma Z2slst_len2 : forall z n, 0 < z < 2 ^^ n -> (length (Z2slst z) <= n.+1)%coq_nat.

correctness of the addition for signed numbers

Lemma slst2Z_last : forall l e, l <> nil ->
  [[ l ++ e :: nil ]]s = 2 * [[ l ]]s + [[ e :: nil ]]u.

Lemma add_lst'_Z_oo: forall n l k carry,
  length l = n -> length k = n ->
  (0 < n)%coq_nat ->
  [[ rev l ]]u + [[ rev k ]]u + [[ carry::nil ]]u < 2^^n ->
  [[ rev (add_lst' (l ++ o ::nil) (k ++ o ::nil) carry) ]]s =
  [[ rev l ]]u + [[ rev k ]]u + [[ carry::nil ]]u.

Lemma add_lst_Z_oo : forall n l k c , length l = n -> length k = n ->
  (n > 0)%coq_nat -> [[ l ]]u + [[ k ]]u + [[ c :: nil ]]u < 2 ^^ n ->
  [[ add_lst (o :: l) (o :: k) c ]]s = [[ l ]]u + [[ k ]]u + [[ c :: nil ]]u.

Lemma add_lst'_Z_oi : forall n l k c, length l = n -> length k = n ->
  (0 < n)%coq_nat -> [[ rev (add_lst' (l ++ o :: nil) (k ++ i :: nil) c) ]]s =
  [[ rev l ]]u + [[ rev k ]]u + [[ c :: nil ]]u - 2 ^^ n.

Lemma add_lst_Z_oi : forall n l k c, length l = n -> length k = n ->
  (0 < n)%coq_nat ->
  [[ add_lst (o :: l) (i :: k) c ]]s =
  [[ l ]]u + [[ k ]]u + [[ c :: nil ]]u - 2 ^^ n.

Lemma add_lst'_Z_ii : forall n l k c, length l = n -> length k = n ->
  (0 < n)%coq_nat ->
  2 ^^ n <= [[ rev l ]]u + [[ rev k ]]u + [[ c :: nil ]]u ->
  [[ rev (add_lst' (l ++ i :: nil) (k ++ i :: nil) c) ]]s =
  [[ rev l ]]u + [[ rev k ]]u + [[ c :: nil ]]u - 2 ^^ (S n).

Lemma add_lst_Z_ii : forall n l k c, length l = n -> length k = n ->
  (O < n)%coq_nat -> 2 ^^ n <= [[ l ]]u + [[ k ]]u + [[ c :: nil ]]u ->
  [[ add_lst (i :: l) (i :: k) c ]]s =
  [[ l ]]u + [[ k ]]u + [[ c :: nil ]]u - 2 ^^ (S n).

Lemma add_lst_Z : forall n a b, length a = S n -> length b = S n ->
  - 2 ^^ n <= [[ a ]]s + [[ b ]]s < 2 ^^ n ->
  [[ add_lst a b o ]]s = [[ a ]]s + [[ b ]]s.

Lemma sext_lst_s2Z : forall l n, [[ sext_lst n l ]]s = [[ l ]]s.

correctness of the signed multiplication

Lemma smul_lst_Z1 : forall n a b, length a = S (S n) -> length b = S (S n) ->
  ~ (is_pos a = true ) -> is_pos b = true ->
  [[ smul_lst a b ]]s = [[ a ]]s * [[ b ]]s.

Lemma smul_lst_Z : forall n a b, length a = n -> length b = n ->
  [[ smul_lst a b ]]s = [[ a ]]s * [[ b ]]s.

Examples:

Eval compute in ([[ i :: i :: i :: i :: nil ]]u).
Eval compute in ([[ i :: i :: i :: i :: nil ]]u).
Eval compute in ([[ o :: o :: o :: i :: nil ]]s).
Eval compute in (listbit_lt (i :: i :: i :: i :: nil) (o :: o :: o :: i :: nil)).
Eval compute in ([[ i :: o :: i :: i :: nil ]]s).
Eval compute in ([[ adjust_slist (i :: o :: i :: i :: nil) 3 ]]s).
Eval compute in ([[ adjust_slist (i :: o :: i :: i :: nil) 2 ]]s).