The abstract of the Mizar article:

High-Speed Algorithms for RSA Cryptograms

by

Yasushi Fuwa, and

Yoshinori Fujisawa

Received February 1, 2000

MML identifier: RADIX_2

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM_1, NAT_1, INT_1, ARYTM_3, FINSEQ_1, RADIX_1, POWER, MIDSP_3,
      RELAT_1, FUNCT_1, RLVECT_1, RADIX_2, FINSEQ_4, GROUP_1;
 notation TARSKI, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1,
      FUNCT_1, POWER, FINSEQ_1, FINSEQ_4, BINARITH, EULER_2, RVSUM_1, TREES_4,
      WSIERP_1, RADIX_1, MIDSP_3;
 constructors REAL_1, POWER, BINARITH, FINSEQ_4, EULER_2, RADIX_1, SEQ_1,
      MEMBERED, RAT_1;
 clusters INT_1, RELSET_1, XREAL_0, WSIERP_1, NAT_1, MEMBERED, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Some Useful Theorems

reserve k for Nat;

theorem :: RADIX_2:1
    for a be Nat holds a mod 1 = 0;

theorem :: RADIX_2:2
  for a,b be Integer, n be Nat st n>0 holds
    ((a mod n)+(b mod n)) mod n = (a + (b mod n)) mod n &
    ((a mod n)+(b mod n)) mod n = ((a mod n) + b) mod n;

theorem :: RADIX_2:3
  for a,b be Integer, n be Nat st n>0 holds
    (a*b) mod n = (a*(b mod n)) mod n &
    (a*b) mod n = ((a mod n)*b) mod n;

theorem :: RADIX_2:4
  for a,b,i be Nat st 1 <= i & 0 < b holds
    (a mod (b |^ i)) div (b |^ (i -'1)) = (a div (b |^ (i -'1))) mod b;

theorem :: RADIX_2:5
  for i,n be Nat st i in Seg n holds i+1 in Seg (n+1);

begin :: Properties of Addition operation using radix-2^k SD numbers

theorem :: RADIX_2:6
  for k be Nat holds Radix(k) > 0;

theorem :: RADIX_2:7
  for x be Tuple of 1,k-SD holds SDDec(x) = DigA(x,1);

theorem :: RADIX_2:8
  for x be Integer holds
    SD_Add_Data(x,k) + SD_Add_Carry(x)*Radix(k) = x;

theorem :: RADIX_2:9
  for n be Nat
    for x be Tuple of (n+1),k-SD, xn be Tuple of n,k-SD st
      (for i be Nat st i in Seg n holds x.i = xn.i) holds
        Sum DigitSD(x) = Sum(DigitSD(xn)^<*SubDigit(x,n+1,k)*>);

theorem :: RADIX_2:10
  for n be Nat
    for x be Tuple of (n+1),k-SD, xn be Tuple of n,k-SD st
      (for i be Nat st i in Seg n holds x.i = xn.i) holds
        SDDec(xn) + (Radix(k) |^ n)*DigA(x,n+1) = SDDec(x);

theorem :: RADIX_2:11
    for n be Nat st n >= 1 holds
    for x,y be Tuple of n,k-SD st k >= 2 holds
      SDDec(x '+' y) + SD_Add_Carry(DigA(x,n) + DigA(y,n))
        *(Radix(k) |^ n) = SDDec(x) + SDDec(y);

begin :: Definitions on the relation between a FinSequence of k-SD and
      :: a FinSequence of NAT and some properties about them

definition let i,k,n be Nat, x be Tuple of n,NAT;
  func SubDigit2(x,i,k) -> Element of NAT equals
:: RADIX_2:def 1

    (Radix(k) |^ (i -'1))*(x.i);
end;

definition let n,k be Nat, x be Tuple of n,NAT;
  func DigitSD2(x,k) -> Tuple of n,NAT means
:: RADIX_2:def 2

    for i be Nat st i in Seg n holds it/.i = SubDigit2(x,i,k);
end;

definition let n,k be Nat, x be Tuple of n,NAT;
  func SDDec2(x,k) -> Nat equals
:: RADIX_2:def 3

    Sum DigitSD2(x,k);
end;

definition let i,k,x be Nat;
  func DigitDC2(x,i,k) -> Nat equals
:: RADIX_2:def 4

    (x mod (Radix(k) |^ i)) div (Radix(k) |^ (i -'1));
end;

definition let k,n,x be Nat;
  func DecSD2(x,n,k) -> Tuple of n,NAT means
:: RADIX_2:def 5

    for i be Nat st i in Seg n holds it.i = DigitDC2(x,i,k);
end;

theorem :: RADIX_2:12
  for n,k be Nat, x be Tuple of n,NAT, y be Tuple of n,k-SD
    st x = y holds DigitSD2(x,k) = DigitSD(y);

theorem :: RADIX_2:13
  for n,k be Nat, x be Tuple of n,NAT, y be Tuple of n,k-SD
    st x = y holds SDDec2(x,k) = SDDec(y);

theorem :: RADIX_2:14
  for x,n,k be Nat holds DecSD2(x,n,k) = DecSD(x,n,k);

theorem :: RADIX_2:15
  for n be Nat st n >= 1 holds
    for m,k be Nat st m is_represented_by n,k holds
      m = SDDec2(DecSD2(m,n,k),k);

begin :: Algorithm of calculation of (a*b) mod c based on
      :: radix-2^k SD numbers and its correctness

definition let q be Integer, f,j,k,n be Nat, c be Tuple of n,k-SD;
  func Table1(q,c,f,j) -> Integer equals
:: RADIX_2:def 6

    (q*DigA(c,j)) mod f;
end;

definition let q be Integer, k,f,n be Nat, c be Tuple of n,k-SD;
  assume n >= 1;
  func Mul_mod(q,c,f,k) -> Tuple of n,INT means
:: RADIX_2:def 7

    it.1 = Table1(q,c,f,n) &
    for i be Nat st 1 <= i & i <= n - 1 holds
      ex I1,I2 be Integer st I1 = it.i & I2 = it.(i+1) &
        I2 = (Radix(k)*I1+Table1(q,c,f,n -'i)) mod f;
end;

theorem :: RADIX_2:16
    for n be Nat st n >= 1 holds
    for q be Integer, ic,f,k be Nat
      st ic is_represented_by n,k & f > 0 holds
       for c be Tuple of n,k-SD st c = DecSD(ic,n,k) holds
         Mul_mod(q,c,f,k).n = (q * ic) mod f;

begin :: Algorithm of calculation of (a^b) mod c based on
      :: radix-2^k SD numbers and its correctness

definition let n,f,j,m be Nat, e be Tuple of n,NAT;
  func Table2(m,e,f,j) -> Nat equals
:: RADIX_2:def 8

    (m |^ (e/.j)) mod f;
end;

definition let k,f,m,n be Nat, e be Tuple of n,NAT;
  assume n >= 1;
  func Pow_mod(m,e,f,k) -> Tuple of n,NAT means
:: RADIX_2:def 9

    it.1 = Table2(m,e,f,n) &
    for i be Nat st 1 <= i & i <= n - 1 holds
      ex i1,i2 be Nat st i1 = it.i & i2 = it.(i+1) &
        i2 = (((i1 |^ Radix(k)) mod f) * Table2(m,e,f,n-'i)) mod f;
end;

theorem :: RADIX_2:17
    for n be Nat st n >= 1 holds
    for m,k,f,ie be Nat st ie is_represented_by n,k & f>0 holds
      for e be Tuple of n,NAT st e = DecSD2(ie,n,k) holds
        Pow_mod(m,e,f,k).n = (m |^ ie) mod f;