Require Export Correctness.
Require Export fun.
Coercion inject_nat : nat >-> Z.
Parameter beta':Z.
Axiom betaGt1:`1<beta'`.
Definition beta := `2*beta'`.
Definition modZ := {x:Z | `0<=x`/\`x<beta`}.
Definition modZtoZ := [y:modZ]Cases y of (exist x _) => x end.
Parameter bound : Z.
Global Variable m : array bound of modZ.
Global Variable rb : bool ref.
Global Variable rz : Z ref.
Fixpoint I [A:(array bound modZ);position:nat;lenght:nat] : Z :=
Cases lenght of O => ZERO
| (S l') => Cases (access A position) of
(exist modZ _) =>
(Zplus (Zmult beta (I A (S position) l')) modZ)
end
end.
Definition Zmultbool :=
[c:bool] [n:Z]
Cases c of
true => n
| false => ZERO
end.
Definition no_overlap := [p1,p2,l1,l2:nat](p1=p2)\/`p1+l1<=p2`\/`p2+l2<=p1`.
Global Variable mpn_sqrtrem2 :
fun (pos_s:nat)(pos_r:nat)(pos_n:nat)
returns _:unit
reads m
writes m, rb
pre `pos_n+2<=bound`/\`pos_s+1<=bound`/\`pos_r+1<=bound`/\
(no_overlap pos_r pos_s (S O) (S O))
/\(IsNormalized (I m pos_n (2)) (pow beta (2)))
post (I m@ pos_n (2))=
(Zplus (Zmult (I m pos_s (1))
(I m pos_s (1)))
(Zplus (I m pos_r (1))
(Zmultbool rb beta))) /\
(Zle (Zplus (I m pos_r (1)) (Zmultbool rb beta))
(Zmult `2` (I m pos_s (1))))
/\
((p:nat)`0<=p<bound`->((lt p pos_n)\/(le (plus pos_n (2)) p))->
(access m p)=(access m@ p))
end.
Global Variable mpn_sub_n :
fun (pos_r:nat)(pos_a:nat)(pos_b:nat)(l:nat)
returns _: unit
reads m
writes m, rb
pre `pos_a+l<=bound`/\`pos_b+l<=bound`
/\`pos_r+l<=bound`
/\(no_overlap pos_r pos_a l l)
/\(no_overlap pos_r pos_b l l)
/\(no_overlap pos_a pos_b l l)
post (I m pos_r l)=
(Zminus (Zplus (Zmultbool rb (pow beta l))
(I m@ pos_a l))
(I m@ pos_b l))
/\
((p:nat)`0<=p<bound`->((lt p pos_r)\/(le (plus pos_r (l)) p))->
(access m p)=(access m@ p))
end.
Global Variable mpn_divrem :
fun (pos_q:nat)(pos_a:nat)(la:nat)(pos_b:nat)(lb:nat)
returns _:unit
reads m
writes m,rb
pre `pos_a+la<=bound`
/\`pos_b+lb<=bound`
/\`pos_q+(la-lb)<=bound`
/\`lb<=la`
/\`(pow beta lb)<=2*(I m pos_b lb)`
/\(no_overlap pos_a pos_b la lb)
/\(no_overlap pos_q pos_a (minus la lb) la)
/\(no_overlap pos_q pos_b (minus la lb) lb)
post ((I m@ pos_a la)=
(Zplus
(Zmult
(Zplus (Zmultbool rb (pow beta (minus la lb)))
(I m pos_q (minus la lb)))
(I m@ pos_b lb))
(I m pos_a lb)))
/\(Zlt (I m pos_a lb)
(I m@ pos_b lb))
/\((p:nat)`0<=p<bound`->((lt p pos_q)\/(le (plus pos_q (minus la lb)) p))
/\((lt p pos_a)\/(le (plus pos_a lb) p))
->(access m p)=(access m@ p))
end.
Global Variable mpn_add_n :
fun (pos_r:nat)(pos_b:nat)(pos_a:nat)(l:nat)
returns _:unit
reads m
writes m,rb
pre `pos_a+l<=bound`
/\`pos_b+l<=bound`
/\`pos_r+l<=bound`
/\(no_overlap pos_r pos_a l l)
/\(no_overlap pos_r pos_b l l)
/\(no_overlap pos_a pos_b l l)
post (Zplus (I m@ pos_a l)
(I m@ pos_b l))=
(Zplus (Zmultbool rb (pow beta l))
(I m pos_r l))
/\(p:nat)`0<=p<bound`->((lt p pos_r)\/(le (plus pos_r l) p))
->(access m p)=(access m@ p)
end.
Global Variable mpn_mul_n :
fun (pos_r:nat)(pos_a:nat)(pos_b:nat)(l:nat)
returns tt:unit
reads m
writes m
pre `pos_a+l<=bound`
/\`pos_b+l<=bound`
/\`pos_r+2*l<=bound`
/\(no_overlap pos_r pos_a l l)
/\(no_overlap pos_r pos_b l l)
/\(no_overlap pos_a pos_b l l)
post (Zmult (I m@ pos_a l)
(I m@ pos_b l))
=(I m pos_r (mult (2) l))
/\(p:nat)`0<=p<bound`->((lt p pos_r)\/(le (plus pos_r (mult (2) l)) p))
->(access m p)=(access m@ p)
end.
Global Variable mpn_sqr_n :
fun (pos_r:nat)(pos_a:nat)(l:nat)
returns tt:unit
reads m
writes m
pre `pos_a+l<=bound`
/\`pos_r+2*l<=bound`
/\(`pos_r+2*l<=pos_a`\/`pos_a+l<=pos_r`)
post (Zsquare (I m@ pos_a l)) = (I m pos_r (mult (2) l))
/\(p:nat)`0<=p<bound`->((lt p pos_r)\/(le (plus pos_r (mult (2) l)) p))
->(access m p)=(access m@ p)
end.
Global Variable mpn_sub_1 :
fun (pos_r:nat)(pos_a:nat)(l:nat)(limb:Z)
returns _: unit
reads m
writes m, rb
pre `pos_a+l<=bound`
/\`pos_r+l<=bound`
/\`0<=limb<beta`
/\(no_overlap pos_r pos_a l l)
post (I m pos_r l)
= (Zminus (Zplus (Zmultbool rb (pow beta l))
(I m@ pos_a l))
limb)
/\(p:nat)`0<=p<bound`->((lt p pos_r)\/(le (plus pos_r l) p))
->(access m p)=(access m@ p)
end.
Global Variable mpn_add_1 :
fun (pos_r:nat)(pos_a:nat)(l:nat)(limb:Z)
returns _:unit
reads m
writes m, rb
pre `pos_a+l<=bound`
/\`pos_r+l<=bound`
/\`0<=limb<beta`
/\(no_overlap pos_r pos_a l l)
post (Zplus (Zmultbool rb (pow beta l))
(I m pos_r l))
= (Zplus (I m@ pos_a l)
limb)
/\(p:nat)`0<=p<bound`->((lt p pos_r)\/(le (plus pos_r l) p))
->(access m p)=(access m@ p)
end.
Definition Post_mpn_addmul_1 := [m:(array bound modZ)]
[m@:(array bound modZ)][pos_r:nat][pos_a:nat][l:nat][limb:Z][result:Z]
(Zplus (Zmult result (pow beta l))
(I m pos_r l))
= (Zplus (I m@ pos_r l)
(Zmult (I m@ pos_a l) limb))
/\(p:nat)`0<=p<bound`->((lt p pos_r)\/(le (plus pos_r l) p))
->(access m p)=(access m@ p).
Global Variable mpn_addmul_1 :
fun (pos_r:nat)(pos_a:nat)(l:nat)(limb:Z)
returns res:Z
reads m
writes m
pre `pos_a+l<=bound`
/\`pos_r+l<=bound`
/\`0<=limb<beta`
/\(no_overlap pos_r pos_a l l)
post (Post_mpn_addmul_1 m m@ pos_r pos_a l limb res)
end.
Lemma modZ_ZERO : `0<=0`/\`0<beta`.
Lemma modZ_xH : `0<=1`/\`1<beta`.
Definition isEvenOrOdd :=
[A:(array bound modZ)][pos_a:nat]
<[_:modZ]modZ>Cases (access A pos_a) of
(exist (POS (xI _)) _) => (exist Z ([x:Z]`0<=x`/\`x<beta`) (POS xH) modZ_xH)
| (exist (POS (xO _)) _) => (exist Z ([x:Z]`0<=x`/\`x<beta`) ZERO modZ_ZERO)
| (exist (POS xH) _) =>(exist Z ([x:Z]`0<=x`/\`x<beta`) (POS xH) modZ_xH)
| (exist ZERO _) => (exist Z ([x:Z]`0<=x`/\`x<beta`) ZERO modZ_ZERO)
| (exist (NEG _) _) => (exist Z ([x:Z]`0<=x`/\`x<beta`) ZERO modZ_ZERO)
end.
Global Variable single_and_1 :
fun (pos_a:nat)
returns _:unit
reads m
writes rz
pre `pos_a<=bound`
post rz = (modZtoZ (isEvenOrOdd m pos_a))
end.
Definition f' : positive -> Z :=
[p:positive]Cases p of xH => beta'
| (xI p) => beta'
| (xO p) => ZERO
end.
Definition aux_shift_1 : Z -> Z :=
[n:Z]Cases n of (POS x) => (f' x)
| ZERO => ZERO
| (NEG x) => (f' x)
end.
Global Variable shift_1 :
fun (v:Z)
returns r:modZ
post (modZtoZ r)=(aux_shift_1 v)
end.
Definition shift_2 := Zdiv2.
Global Variable I_or :
fun (p:nat)(y:modZ)
returns w:modZ
reads m
pre `(modZtoZ (access m p))<beta'`
/\(Ex [yb:Z] (`0<=yb<=1` -> `(modZtoZ y)=yb*beta'`))
post `(modZtoZ w) = (modZtoZ (access m p)) + (modZtoZ y)`
end.
Global Variable mpn_rshift2 :
fun (pos_a:nat)(pos_b:nat)(l:nat)
returns tt:unit
reads m
writes m
pre `pos_b<=pos_a`
/\`pos_a+l<=bound`
/\`pos_b+l<=bound`
/\(no_overlap pos_a pos_b l l)
post `(I m@ pos_b l) = 2*(I m pos_a l)+(modZtoZ (isEvenOrOdd m@ pos_b))`
/\(p:nat)`0<=p<bound`->((lt p pos_a)\/(le (plus pos_a l) p))->
(access m p)=(access m@ p)
end.