Library Corelib.Numbers.Cyclic.Int63.Uint63Axioms
From Corelib Require Import BinNums PosDef IntDef.
From Corelib Require Export PrimInt63.
Local Open Scope Z_scope.
Local Notation "0" := Z0 : Z_scope.
Local Notation "1" := (Zpos 1) : Z_scope.
Local Notation "2" := (Zpos 2) : Z_scope.
Local Infix "+" := Z.add : Z_scope.
Local Infix "-" := Z.sub : Z_scope.
Local Infix "*" := Z.mul : Z_scope.
Local Infix "^" := Z.pow : Z_scope.
Local Infix "<=" := Z.le : Z_scope.
Local Infix "<" := Z.lt : Z_scope.
Local Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
Definition size := 63%nat.
The number of digits as an int
The biggest int
Access to the nth digits
Definition get_digit x p := ltb 0 (land x (lsl 1 p)).
Definition set_digit x p (b:bool) :=
if if leb 0 p then ltb p digits else false then
if b then lor x (lsl 1 p)
else land x (lxor max_int (lsl 1 p))
else x.
Definition set_digit x p (b:bool) :=
if if leb 0 p then ltb p digits else false then
if b then lor x (lsl 1 p)
else land x (lxor max_int (lsl 1 p))
else x.
Translation to Z
Definition is_zero (i:int) := eqb i 0.
Definition is_even (i:int) := is_zero (land i 1).
Fixpoint to_Z_rec (n:nat) (i:int) :=
match n with
| O => 0
| S n =>
(if is_even i then Z.double else Z.succ_double) (to_Z_rec n (lsr i 1))
end.
Definition to_Z := to_Z_rec size.
Fixpoint of_pos_rec (n:nat) (p:positive) {struct p} :=
match n, p with
| O, _ => 0%uint63
| S n, xH => 1%uint63
| S n, xO p => lsl (of_pos_rec n p) 1
| S n, xI p => lor (lsl (of_pos_rec n p) 1) 1
end.
Definition of_pos := of_pos_rec size.
Definition of_Z z :=
match z with
| Zpos p => of_pos p
| 0 => 0%uint63
| Zneg p => sub 0 (of_pos p)
end.
Definition wB := 2 ^ (Z.of_nat size).
Axiom of_to_Z : forall x, of_Z (to_Z x) = x.
Definition is_even (i:int) := is_zero (land i 1).
Fixpoint to_Z_rec (n:nat) (i:int) :=
match n with
| O => 0
| S n =>
(if is_even i then Z.double else Z.succ_double) (to_Z_rec n (lsr i 1))
end.
Definition to_Z := to_Z_rec size.
Fixpoint of_pos_rec (n:nat) (p:positive) {struct p} :=
match n, p with
| O, _ => 0%uint63
| S n, xH => 1%uint63
| S n, xO p => lsl (of_pos_rec n p) 1
| S n, xI p => lor (lsl (of_pos_rec n p) 1) 1
end.
Definition of_pos := of_pos_rec size.
Definition of_Z z :=
match z with
| Zpos p => of_pos p
| 0 => 0%uint63
| Zneg p => sub 0 (of_pos p)
end.
Definition wB := 2 ^ (Z.of_nat size).
Axiom of_to_Z : forall x, of_Z (to_Z x) = x.
Specification of logical operations
Axiom lsl_spec : forall x p, to_Z (lsl x p) = Z.modulo (to_Z x * 2 ^ to_Z p) wB.
Axiom lsr_spec : forall x p, to_Z (lsr x p) = Z.div (to_Z x) (2 ^ to_Z p).
Definition bit i n := negb (is_zero (lsl (lsr i n) (sub digits 1))).
Axiom land_spec : forall x y i, bit (land x y) i = andb (bit x i) (bit y i).
Axiom lor_spec : forall x y i, bit (lor x y) i = orb (bit x i) (bit y i).
Axiom lxor_spec : forall x y i, bit (lxor x y) i = xorb (bit x i) (bit y i).
Specification of basic opetations
Axiom add_spec : forall x y, to_Z (add x y) = Z.modulo (to_Z x + to_Z y) wB.
Axiom sub_spec : forall x y, to_Z (sub x y) = Z.modulo (to_Z x - to_Z y) wB.
Axiom mul_spec : forall x y, to_Z (mul x y) = Z.modulo (to_Z x * to_Z y) wB.
Axiom mulc_spec : forall x y,
to_Z x * to_Z y = to_Z (fst (mulc x y)) * wB + to_Z (snd (mulc x y)).
Axiom div_spec : forall x y, to_Z (div x y) = Z.div (to_Z x) (to_Z y).
Axiom mod_spec : forall x y,
to_Z (PrimInt63.mod x y) = Z.modulo (to_Z x) (to_Z y).
Axiom eqb_correct : forall i j, eqb i j = true -> i = j.
Axiom eqb_refl : forall x, eqb x x = true.
Axiom ltb_spec : forall x y, ltb x y = true <-> to_Z x < to_Z y.
Axiom leb_spec : forall x y, leb x y = true <-> to_Z x <= to_Z y.
Exotic operations
Axioms on operations which are just short cut
Definition compare_def x y :=
if ltb x y then Lt else if eqb x y then Eq else Gt.
Axiom compare_def_spec : forall x y, compare x y = compare_def x y.
Axiom head0_spec : forall x, 0 < to_Z x ->
Z.div wB 2 <= 2 ^ (to_Z (head0 x)) * to_Z x < wB.
Axiom tail0_spec : forall x, 0 < to_Z x ->
exists y, Z0 <= y /\ to_Z x = (2 * y + 1) * (2 ^ to_Z (tail0 x)).
Definition addc_def x y :=
let r := add x y in
if ltb r x then C1 r else C0 r.
Axiom addc_def_spec : forall x y, addc x y = addc_def x y.
Definition addcarry i j := add (add i j) 1.
Definition addcarryc_def x y :=
let r := addcarry x y in
if leb r x then C1 r else C0 r.
Axiom addcarryc_def_spec : forall x y, addcarryc x y = addcarryc_def x y.
Definition subc_def x y := if leb y x then C0 (sub x y) else C1 (sub x y).
Axiom subc_def_spec : forall x y, subc x y = subc_def x y.
Definition subcarryc_def x y :=
if ltb y x then C0 (sub (sub x y) 1) else C1 (sub (sub x y) 1).
Axiom subcarryc_def_spec : forall x y, subcarryc x y = subcarryc_def x y.
Definition diveucl_def x y := (div x y, PrimInt63.mod x y).
Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y.
Axiom diveucl_21_spec : forall a1 a2 b,
let (q,r) := diveucl_21 a1 a2 b in
let (q',r') := Z.div_eucl (to_Z a1 * wB + to_Z a2) (to_Z b) in
to_Z a1 < to_Z b -> to_Z q = q' /\ to_Z r = r'.
Definition addmuldiv_def p x y :=
lor (lsl x p) (lsr y (sub digits p)).
Axiom addmuldiv_def_spec : forall p x y,
addmuldiv p x y = addmuldiv_def p x y.