# Module specifications

``` 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. ```

``` ```

Index