# Signature and specification of a bounded integer structure

This file specifies how to represent Z/nZ when n=2^d, d being the number of digits of these bounded integers.

Require Import ZArith.
Require Import Znumtheory.
Require Import BigNumPrelude.
Require Import DoubleType.

Local Open Scope Z_scope.

First, a description via an operator record and a spec record.

Module ZnZ.

Class Ops (t:Type) := MkOps {

digits : positive;
zdigits: t;
to_Z : t -> Z;
of_pos : positive -> N * t;
tail0 : t -> t;

zero : t;
one : t;
minus_one : t;

compare : t -> t -> comparison;
eq0 : t -> bool;

opp_c : t -> carry t;
opp : t -> t;
opp_carry : t -> t;

succ_c : t -> carry t;
add_c : t -> t -> carry t;
add_carry_c : t -> t -> carry t;
succ : t -> t;
add : t -> t -> t;
add_carry : t -> t -> t;

pred_c : t -> carry t;
sub_c : t -> t -> carry t;
sub_carry_c : t -> t -> carry t;
pred : t -> t;
sub : t -> t -> t;
sub_carry : t -> t -> t;

mul_c : t -> t -> zn2z t;
mul : t -> t -> t;
square_c : t -> zn2z t;

div21 : t -> t -> t -> t*t;
div_gt : t -> t -> t * t;
div : t -> t -> t * t;

modulo_gt : t -> t -> t;
modulo : t -> t -> t;

gcd_gt : t -> t -> t;
gcd : t -> t -> t;

add_mul_div : t -> t -> t -> t;

pos_mod : t -> t -> t;

is_even : t -> bool;

sqrt2 : t -> t -> t * carry t;
sqrt : t -> t }.

Section Specs.
Context {t : Type}{ops : Ops t}.

Notation "[| x |]" := (to_Z x) (at level 0, x at level 99).

Let wB := base digits.

Notation "[+| c |]" :=
(interp_carry 1 wB to_Z c) (at level 0, x at level 99).

Notation "[-| c |]" :=
(interp_carry (-1) wB to_Z c) (at level 0, x at level 99).

Notation "[|| x ||]" :=
(zn2z_to_Z wB to_Z x) (at level 0, x at level 99).

Class Specs := MkSpecs {

spec_to_Z : forall x, 0 <= [| x |] < wB;
spec_of_pos : forall p,
Zpos p = (Z_of_N (fst (of_pos p)))*wB + [|(snd (of_pos p))|];
spec_zdigits : [| zdigits |] = Zpos digits;
spec_more_than_1_digit: 1 < Zpos digits;

spec_0 : [|zero|] = 0;
spec_1 : [|one|] = 1;
spec_m1 : [|minus_one|] = wB - 1;

spec_compare : forall x y, compare x y = ([|x|] ?= [|y|]);

spec_eq0 : forall x, eq0 x = true -> [|x|] = 0;

spec_opp_c : forall x, [-|opp_c x|] = -[|x|];
spec_opp : forall x, [|opp x|] = (-[|x|]) mod wB;
spec_opp_carry : forall x, [|opp_carry x|] = wB - [|x|] - 1;

spec_succ_c : forall x, [+|succ_c x|] = [|x|] + 1;
spec_add_c : forall x y, [+|add_c x y|] = [|x|] + [|y|];
spec_add_carry_c : forall x y, [+|add_carry_c x y|] = [|x|] + [|y|] + 1;
spec_succ : forall x, [|succ x|] = ([|x|] + 1) mod wB;
spec_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wB;
forall x y, [|add_carry x y|] = ([|x|] + [|y|] + 1) mod wB;

spec_pred_c : forall x, [-|pred_c x|] = [|x|] - 1;
spec_sub_c : forall x y, [-|sub_c x y|] = [|x|] - [|y|];
spec_sub_carry_c : forall x y, [-|sub_carry_c x y|] = [|x|] - [|y|] - 1;
spec_pred : forall x, [|pred x|] = ([|x|] - 1) mod wB;
spec_sub : forall x y, [|sub x y|] = ([|x|] - [|y|]) mod wB;
spec_sub_carry :
forall x y, [|sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB;

spec_mul_c : forall x y, [|| mul_c x y ||] = [|x|] * [|y|];
spec_mul : forall x y, [|mul x y|] = ([|x|] * [|y|]) mod wB;
spec_square_c : forall x, [|| square_c x||] = [|x|] * [|x|];

spec_div21 : forall a1 a2 b,
wB/2 <= [|b|] ->
[|a1|] < [|b|] ->
let (q,r) := div21 a1 a2 b in
[|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|];
spec_div_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
let (q,r) := div_gt a b in
[|a|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|];
spec_div : forall a b, 0 < [|b|] ->
let (q,r) := div a b in
[|a|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|];

spec_modulo_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
[|modulo_gt a b|] = [|a|] mod [|b|];
spec_modulo : forall a b, 0 < [|b|] ->
[|modulo a b|] = [|a|] mod [|b|];

spec_gcd_gt : forall a b, [|a|] > [|b|] ->
Zis_gcd [|a|] [|b|] [|gcd_gt a b|];
spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|];

spec_head00: forall x, [|x|] = 0 -> [|head0 x|] = Zpos digits;
spec_head0 : forall x, 0 < [|x|] ->
wB/ 2 <= 2 ^ ([|head0 x|]) * [|x|] < wB;
spec_tail00: forall x, [|x|] = 0 -> [|tail0 x|] = Zpos digits;
spec_tail0 : forall x, 0 < [|x|] ->
exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail0 x|]) ;
spec_add_mul_div : forall x y p,
[|p|] <= Zpos digits ->
[| add_mul_div p x y |] =
([|x|] * (2 ^ [|p|]) +
[|y|] / (2 ^ ((Zpos digits) - [|p|]))) mod wB;
spec_pos_mod : forall w p,
[|pos_mod p w|] = [|w|] mod (2 ^ [|p|]);

spec_is_even : forall x,
if is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1;
spec_sqrt2 : forall x y,
wB/ 4 <= [|x|] ->
let (s,r) := sqrt2 x y in
[||WW x y||] = [|s|] ^ 2 + [+|r|] /\
[+|r|] <= 2 * [|s|];
spec_sqrt : forall x,
[|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2
}.

End Specs.

Generic construction of double words

Section WW.

Context {t : Type}{ops : Ops t}{specs : Specs ops}.

Let wB := base digits.

Definition WO' (eq0:t->bool) zero h :=
if eq0 h then W0 else WW h zero.

Definition WO := Eval lazy beta delta [WO'] in
let eq0 := ZnZ.eq0 in
let zero := ZnZ.zero in
WO' eq0 zero.

Definition OW' (eq0:t->bool) zero l :=
if eq0 l then W0 else WW zero l.

Definition OW := Eval lazy beta delta [OW'] in
let eq0 := ZnZ.eq0 in
let zero := ZnZ.zero in
OW' eq0 zero.

Definition WW' (eq0:t->bool) zero h l :=
if eq0 h then OW' eq0 zero l else WW h l.

Definition WW := Eval lazy beta delta [WW' OW'] in
let eq0 := ZnZ.eq0 in
let zero := ZnZ.zero in
WW' eq0 zero.

Lemma spec_WO : forall h,
zn2z_to_Z wB to_Z (WO h) = (to_Z h)*wB.

Lemma spec_OW : forall l,
zn2z_to_Z wB to_Z (OW l) = to_Z l.

Lemma spec_WW : forall h l,
zn2z_to_Z wB to_Z (WW h l) = (to_Z h)*wB + to_Z l.

End WW.

Injecting Z numbers into a cyclic structure

Section Of_Z.

Context {t : Type}{ops : Ops t}{specs : Specs ops}.

Notation "[| x |]" := (to_Z x) (at level 0, x at level 99).

Theorem of_pos_correct:
forall p, Zpos p < base digits -> [|(snd (of_pos p))|] = Zpos p.

Definition of_Z z :=
match z with
| Zpos p => snd (of_pos p)
| _ => zero
end.

Theorem of_Z_correct:
forall p, 0 <= p < base digits -> [|of_Z p|] = p.

End Of_Z.

End ZnZ.

A modular specification grouping the earlier records.

Module Type CyclicType.
Parameter t : Type.
Declare Instance ops : ZnZ.Ops t.
Declare Instance specs : ZnZ.Specs ops.
End CyclicType.

A Cyclic structure can be seen as a ring

Module CyclicRing (Import Cyclic : CyclicType).

Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99).

Definition eq (n m : t) := [| n |] = [| m |].

Local Infix "==" := eq (at level 70).
Local Notation "0" := ZnZ.zero.
Local Notation "1" := ZnZ.one.
Local Infix "-" := ZnZ.sub.
Local Notation "- x" := (ZnZ.opp x).
Local Infix "*" := ZnZ.mul.
Local Notation wB := (base ZnZ.digits).

Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul
ZnZ.spec_opp ZnZ.spec_sub
: cyclic.

Ltac zify := unfold eq in *; autorewrite with cyclic.

Lemma add_0_l : forall x, 0 + x == x.

Lemma add_comm : forall x y, x + y == y + x.

Lemma add_assoc : forall x y z, x + (y + z) == x + y + z.

Lemma mul_1_l : forall x, 1 * x == x.

Lemma mul_comm : forall x y, x * y == y * x.

Lemma mul_assoc : forall x y z, x * (y * z) == x * y * z.

Lemma mul_add_distr_r : forall x y z, (x+y)*z == x*z + y*z.

Lemma add_opp_r : forall x y, x + - y == x-y.

Lemma add_opp_diag_r : forall x, x + - x == 0.

Lemma CyclicRing : ring_theory 0 1 ZnZ.add ZnZ.mul ZnZ.sub ZnZ.opp eq.

Definition eqb x y :=
match ZnZ.compare x y with Eq => true | _ => false end.

Lemma eqb_eq : forall x y, eqb x y = true <-> x == y.

Lemma eqb_correct : forall x y, eqb x y = true -> x==y.

End CyclicRing.