Library Numeric


Common interface for numerics domains. A part of Bicolano project by David Pichardie, adapted to fit into CoJaq project.
Require Export ZArith BinPosDef BinNums.
Require Import Common List.
Import List.ListNotations.

Open Local Scope Z_scope.

Signature

Signature for modules implementing integers modulo 2^N.
Module Type NUMERIC.

Original Bicolano staff

  Parameter t : Set.
  Parameter toZ : tZ.
  Parameter power : Z.
  Parameter power_positive: power > 0.
  Definition half_base := 2^power.
  Definition base := 2×half_base.
  Definition range (z:Z) : Prop := -half_base z < half_base.
  Parameter range_prop : x:t, range (toZ x).

  Definition smod (x:Z) : Z :=
     let z := x mod base in
      match Zcompare z half_base with
     | Ltz
     | _z - base
     end.

  Parameter add : ttt.
  Parameter add_prop : i1 i2,
    toZ (add i1 i2)= smod (toZ i1 + toZ i2).

  Parameter sub : ttt.
  Parameter sub_prop : i1 i2,
    toZ (sub i1 i2)= smod (toZ i1 - toZ i2).

  Parameter mul : ttt.
  Parameter mul_prop : i1 i2,
    toZ (mul i1 i2)= smod (toZ i1 × toZ i2).

  Parameter div : ttt.
  Parameter div_prop : i1 i2,
    toZ (div i1 i2)= smod (toZ i1 / toZ i2).

  Parameter rem : ttt.
  Parameter rem_prop : i1 i2,
    toZ (rem i1 i2)= smod (toZ i1 mod toZ i2).

  Parameter shr : ttt.
  Parameter shr_prop : i1 i2,
    toZ (shr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
  Parameter shl : ttt.
  Parameter shl_prop : i1 i2,
    toZ (shr i1 i2) = smod (toZ i1 × 2^(toZ i2 mod 32)).

  Parameter ushr : ttt.
  Parameter ushr_prop1 : i1 i2,
    toZ i1 < 0 →
    toZ (ushr i1 i2) = smod ((toZ i1 + base) / 2^(toZ i2 mod 32)).
  Parameter ushr_prop2 : i1 i2,
    toZ i1 0 →
    toZ (ushr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).

  Parameter and : ttt.
  Parameter or : ttt.
  Parameter xor : ttt.

  Parameter neg : tt.
  Parameter neg_prop : i,
    toZ (neg i) = smod (- toZ i).

  Parameter const : Zt.
  Parameter const_prop : z,
   range ztoZ (const z) = z.

Added in CoJaq version


  Axiom PToZDistinct: i1 i2,
    toZ i1 = toZ i2i1 = i2.

  Axiom PNumericEqDec: eqDecS t.

Constants

  Parameter zero : t.
  Axiom PzeroToZ: toZ zero = 0.

  Parameter one : t.
  Axiom PoneToZ: toZ one = 1.

  Parameter minus_one : t.
  Axiom PminusOneToZ: toZ minus_one = -1.

  Parameter isNotZero : tProp.
  Axiom PisNotZero: arg, isNotZero arg toZ arg 0.
  Axiom PoneIsNotZero: isNotZero one.

Comparison operators (bool).

  Parameter compare: ttcomparison.
  Parameter is_eq : ttbool.
  Parameter is_ne : ttbool.
  Parameter is_le : ttbool.
  Parameter is_lt : ttbool.
  Parameter is_ge : ttbool.
  Parameter is_gt : ttbool.

  Axiom Pcompare_toZ: arg1 arg2,
    compare arg1 arg2 = Z.compare (toZ arg1) (toZ arg2).

The operation to truncate a number in the current representation to the representation given by p-bit number where p is its second argument
  Parameter truncate : tpositivet.


End NUMERIC.

Implementation

Provides power parameter for NUMERIC module.
Module Type NUMSIZE.
  Parameter power : Z.
  Parameter power_positive: power > 0.
End NUMSIZE.

Creates an actual module implementing NUMERIC for a given power. In fact, the implementation is incomplete (some Parameters and Axioms left).
Module Make (S:NUMSIZE) : NUMERIC with Definition power := S.power.
  Parameter t : Set.
  Parameter toZ : tZ.
  Definition power := S.power.
  Definition half_base := 2^power.
  Definition base := 2×half_base.
  Definition range (z:Z) : Prop := -half_base z < half_base.
  Parameter range_prop : x:t, range (toZ x).
  Lemma power_positive : power > 0.
  Proof.
    apply S.power_positive.
  Qed.

  Definition smod (x:Z) : Z :=
     let z := x mod base in
      match Zcompare z half_base with
     | Ltz
     | _z - base
     end.

  Parameter add : ttt.
  Parameter add_prop : i1 i2,
    toZ (add i1 i2)= smod (toZ i1 + toZ i2).

  Parameter sub : ttt.
  Parameter sub_prop : i1 i2,
    toZ (sub i1 i2)= smod (toZ i1 - toZ i2).

  Parameter mul : ttt.
  Parameter mul_prop : i1 i2,
    toZ (mul i1 i2)= smod (toZ i1 × toZ i2).

  Parameter div : ttt.
  Parameter div_prop : i1 i2,
    toZ (div i1 i2)= smod (toZ i1 / toZ i2).

  Parameter rem : ttt.
  Parameter rem_prop : i1 i2,
    toZ (rem i1 i2)= smod (toZ i1 mod toZ i2).

  Parameter shr : ttt.
  Parameter shr_prop : i1 i2,
    toZ (shr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).
  Parameter shl : ttt.
  Parameter shl_prop : i1 i2,
    toZ (shr i1 i2) = smod (toZ i1 × 2^(toZ i2 mod 32)).

  Parameter ushr : ttt.
  Parameter ushr_prop1 : i1 i2,
    toZ i1 < 0 →
    toZ (ushr i1 i2) = smod ((toZ i1 + base) / 2^(toZ i2 mod 32)).
  Parameter ushr_prop2 : i1 i2,
    toZ i1 0 →
    toZ (ushr i1 i2) = toZ i1 / 2^(toZ i2 mod 32).

  Parameter and : ttt.
  Parameter or : ttt.
  Parameter xor : ttt.

  Parameter neg : tt.
  Parameter neg_prop : i,
    toZ (neg i) = smod (- toZ i).

  Parameter const : Zt.
  Parameter const_prop : z,
   range ztoZ (const z) = z.

  Lemma half_base_ge_2: 2 half_base.
  Proof.
    unfold half_base.
    change (2^1 2^power).
    apply Z.pow_le_mono.
    omega.
    assert (H := power_positive).
    omega.
  Qed.

  Axiom PToZDistinct: i1 i2,
    toZ i1 = toZ i2i1 = i2.

  Axiom PNumericEqDec: eqDecS t.

  Definition zero : t := const 0.
  Lemma PzeroToZ: toZ zero = 0.
  Proof.
    apply const_prop.
    unfold range.
    assert (H := half_base_ge_2).
    omega.
  Qed.

  Definition one : t := const 1.
  Lemma PoneToZ: toZ one = 1.
  Proof.
    apply const_prop.
    unfold range.
    assert (H := half_base_ge_2).
    omega.
  Qed.

  Definition minus_one : t := const (-1).
  Lemma PminusOneToZ: toZ minus_one = -1.
  Proof.
    apply const_prop.
    unfold range.
    assert (H := half_base_ge_2).
    omega.
  Qed.

  Definition isNotZero (arg: t): Prop := toZ arg 0.

  Lemma PisNotZero: arg, isNotZero arg toZ arg 0.
  Proof.
    intuition.
  Qed.

  Lemma PoneIsNotZero: isNotZero one.
  Proof.
    apply PisNotZero.
    rewrite PoneToZ.
    discriminate.
  Qed.

  Definition compare arg1 arg2 :=
    Z.compare (toZ arg1) (toZ arg2).

  Definition is_eq arg1 arg2 :=
    match compare arg1 arg2 with
    | Ltfalse
    | Eqtrue
    | Gtfalse
    end.

  Definition is_ne arg1 arg2 :=
    match compare arg1 arg2 with
    | Lttrue
    | Eqfalse
    | Gttrue
    end.

  Definition is_le arg1 arg2 :=
    match compare arg1 arg2 with
    | Lttrue
    | Eqtrue
    | Gtfalse
    end.

  Definition is_lt arg1 arg2 :=
    match compare arg1 arg2 with
    | Lttrue
    | Eqfalse
    | Gtfalse
    end.

  Definition is_ge arg1 arg2 :=
    match compare arg1 arg2 with
    | Ltfalse
    | Eqtrue
    | Gttrue
    end.

  Definition is_gt arg1 arg2 :=
    match compare arg1 arg2 with
    | Ltfalse
    | Eqfalse
    | Gttrue
    end.

  Lemma Pcompare_toZ: arg1 arg2,
    compare arg1 arg2 = Z.compare (toZ arg1) (toZ arg2).
  Proof.
    auto.
  Qed.

Transforms the given positive x into its list of least significant bits according to the representation in p bits

  Fixpoint digits_of_pos (x:positive) (p:positive) : list bool :=
     let addfalse li := false :: li in
    match x with
    | xO yfalse :: digits_of_pos y (Pos.pred p)
    | xI ytrue :: digits_of_pos y (Pos.pred p)
    | xHmatch p with
            | xHtrue :: nil
            | _true :: Pos.iter (Pos.pred p) addfalse nil
            end
    end.

Lemma testdop45 : (digits_of_pos 4 5) = [false; false; true; false; false].
Proof.
simpl.
trivial.
Qed.

Transforms the given integer x into its list of least significant bits according to the representation in p bits
  Fixpoint digits_of_Z (x:Z) (p:positive) : list bool :=
    let addfalse li := false :: li in
      match x with
      | Z0Pos.iter p addfalse nil
      | Zpos x1digits_of_pos x1 p
      | Zneg x1digits_of_pos ((Pos.pow 2 p) - x1)%positive p
      end.

  Fixpoint pos_of_digits (d:list bool) : positive :=
  match d with
  | nilxH
  | true :: nilxH
  | false :: nilxH
  | true :: tlxI (pos_of_digits tl)
  | false :: tlxO (pos_of_digits tl)
  end.


  Fixpoint clear_false (d:list bool) : list bool :=
  match d with
  | nilnil
  | true :: tld
  | false :: tlclear_false tl
  end.

TODO we assume d is in two's complement
  Fixpoint Z_of_digits (d:list bool) : Z :=
  let rl := rev d in
  let cf := clear_false rl in
  match rl with
  | nilZ0
  | true :: tlZneg (2^(P_of_succ_nat ((length rl) -1)) - (pos_of_digits d))
  | false :: tlmatch cf with
                   | nilZ0
                   | xZpos (pos_of_digits (rev cf))
                   end
  end.

  Definition truncateZ (x:Z) (p:positive) : Z :=
    Z_of_digits (firstn (nat_of_P p) (digits_of_Z x (Pos.of_nat (Z.to_nat power)))).

  Definition truncate (x:t) (p:positive) : t := const (truncateZ (toZ x) p).

Lemma testm75 : power = 5 → (truncateZ (-7) 5) = (-7).
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  trivial.
Qed.

Lemma testm74 : power = 5 → (truncateZ (-7) 4) = (-7).
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  trivial.
Qed.

Lemma testm73 : power = 5 → (truncateZ (-7) 3) = 1.
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  trivial.
Qed.

Lemma testm45 : power = 5 → (truncateZ 4 5) = 4.
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  simpl.
  trivial.
Qed.

Lemma testm44 : power = 5 → (truncateZ 4 4) = 4.
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  simpl.
  trivial.
Qed.

Lemma testm43 : power = 5 → (truncateZ 4 3) = -4.
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  compute.
  trivial.
Qed.

Lemma testm42 : power = 5 → (truncateZ 4 2) = 0.
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  trivial.
Qed.

End Make.

Properties

Properties independent of actual implementation.

Module NumericProperties (_Numeric: NUMERIC).
  Import _Numeric.
  Lemma Pcompare_const: z1 z2,
    range z1range z2
    Z.compare z1 z2 = compare (const z1) (const z2).
  Proof.
    intros z1 z2 Hr1 Hr2.
    rewrite Pcompare_toZ.
    rewrite const_prop.
    rewrite const_prop.
    reflexivity.
    assumption.
    assumption.
  Qed.

  Axiom example_is_eq_t: is_eq zero zero = true.
  Axiom example_is_eq_f: is_eq one zero = false.
  Axiom example_is_ne_t: is_ne one zero = true.
  Axiom example_is_ne_f: is_ne zero zero = false.
  Axiom example_is_le_t: is_le minus_one zero = true.
  Axiom example_is_le_f: is_le one zero = false.
  Axiom example_is_lt_t: is_lt minus_one zero = true.
  Axiom example_is_lt_f: is_lt one zero = false.
  Axiom example_is_ge_t: is_ge one zero = true.
  Axiom example_is_ge_f: is_ge minus_one zero = false.
  Axiom example_is_gt_t: is_gt one zero = true.
  Axiom example_is_gt_f: is_gt minus_one zero = false.

  Axiom is_eq_t_toZ_prop: arg1 arg2,
    is_eq arg1 arg2 = true
    toZ arg1 = toZ arg2.
  Axiom is_eq_f_toZ_prop: arg1 arg2,
    is_eq arg1 arg2 = false
    ¬ toZ arg1 = toZ arg2.

  Axiom is_ne_t_toZ_prop: arg1 arg2,
    is_ne arg1 arg2 = true
    toZ arg1 toZ arg2.
  Axiom is_ne_f_toZ_prop: arg1 arg2,
    is_ne arg1 arg2 = false
    ¬ toZ arg1 toZ arg2.

  Axiom is_le_t_toZ_prop: arg1 arg2,
    is_le arg1 arg2 = true
    toZ arg1 toZ arg2.
  Axiom is_le_f_toZ_prop: arg1 arg2,
    is_le arg1 arg2 = false
    ¬ toZ arg1 toZ arg2.

  Axiom is_lt_t_toZ_prop: arg1 arg2,
    is_lt arg1 arg2 = true
    toZ arg1 < toZ arg2.
  Axiom is_lt_f_toZ_prop: arg1 arg2,
    is_lt arg1 arg2 = false
    ¬ toZ arg1 < toZ arg2.

  Axiom is_ge_t_toZ_prop: arg1 arg2,
    is_ge arg1 arg2 = true
    toZ arg1 toZ arg2.
  Axiom is_ge_f_toZ_prop: arg1 arg2,
    is_ge arg1 arg2 = false
    ¬ toZ arg1 toZ arg2.

  Axiom is_gt_t_toZ_prop: arg1 arg2,
    is_gt arg1 arg2 = true
    toZ arg1 > toZ arg2.
  Axiom is_gt_f_toZ_prop: arg1 arg2,
    is_gt arg1 arg2 = false
    ¬ toZ arg1 > toZ arg2.

End NumericProperties.