:: High-speed algorithms for RSA cryptograms
:: by Yasushi Fuwa and Yoshinori Fujisawa
::
:: Received February 1, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users

theorem :: RADIX_2:1

for a being Nat holds a mod 1 = 0

proof end;

theorem Th2: :: RADIX_2:2

for a, b being Integer
for n being Nat holds ((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n

proof end;

theorem Th3: :: RADIX_2:3

for a, b being Integer
for n being Nat holds (a * b) mod n = (a * (b mod n)) mod n

proof end;

theorem Th4: :: RADIX_2:4

for a, b, i being Nat st 1 <= i & 0 < b holds
(a mod (b |^ i)) div (b |^ (i -' 1)) = (a div (b |^ (i -' 1))) mod b

proof end;

theorem Th5: :: RADIX_2:5

for i, n being Nat st i in Seg n holds
i + 1 in Seg (n + 1)

proof end;

theorem Th6: :: RADIX_2:6

for k being Nat holds Radix k > 0

proof end;

theorem Th7: :: RADIX_2:7

for k being Nat
for x being Tuple of 1,k -SD holds SDDec x = DigA (x,1)

proof end;

theorem Th8: :: RADIX_2:8

for k being Nat
for x being Integer holds (SD_Add_Data (x,k)) + ((SD_Add_Carry x) * (Radix k)) = x

proof end;

theorem Th9: :: RADIX_2:9

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

proof end;

theorem Th10: :: RADIX_2:10

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

proof end;

theorem :: RADIX_2:11

for k, n being Nat st n >= 1 holds
for x, y being 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)

proof end;

:: a FinSequence of NAT and some properties about them

definition

let i, k, n be Nat;
let 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);

coherence
((Radix k) |^ (i -' 1)) * (x . i) is Element of NAT ;

end;

:: deftheorem defines SubDigit2 RADIX_2:def 1 :
for i, k, n being Nat
for x being Tuple of n, NAT holds SubDigit2 (x,i,k) = ((Radix k) |^ (i -' 1)) * (x . i);

definition

let n, k be Nat;
let x be Tuple of n, NAT ;

func DigitSD2 (x,k) -> Tuple of n, NAT means :Def2: :: RADIX_2:def 2
for i being Nat st i in Seg n holds
it /. i = SubDigit2 (x,i,k);

existence
ex b₁ being Tuple of n, NAT st
for i being Nat st i in Seg n holds
b₁ /. i = SubDigit2 (x,i,k)

proof end;

uniqueness
for b₁, b₂ being Tuple of n, NAT st ( for i being Nat st i in Seg n holds
b₁ /. i = SubDigit2 (x,i,k) ) & ( for i being Nat st i in Seg n holds
b₂ /. i = SubDigit2 (x,i,k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines DigitSD2 RADIX_2:def 2 :
for n, k being Nat
for x, b₄ being Tuple of n, NAT holds
( b₄ = DigitSD2 (x,k) iff for i being Nat st i in Seg n holds
b₄ /. i = SubDigit2 (x,i,k) );

definition

let n, k be Nat;
let x be Tuple of n, NAT ;

func SDDec2 (x,k) -> Element of NAT equals :: RADIX_2:def 3
Sum (DigitSD2 (x,k));

coherence
Sum (DigitSD2 (x,k)) is Element of NAT ;

end;

:: deftheorem defines SDDec2 RADIX_2:def 3 :
for n, k being Nat
for x being Tuple of n, NAT holds SDDec2 (x,k) = Sum (DigitSD2 (x,k));

definition

let i, k, x be Nat;

func DigitDC2 (x,i,k) -> Element of NAT equals :: RADIX_2:def 4
(x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));

coherence
(x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of NAT ;

end;

:: deftheorem defines DigitDC2 RADIX_2:def 4 :
for i, k, x being Nat holds DigitDC2 (x,i,k) = (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));

definition

let k, n, x be Nat;

func DecSD2 (x,n,k) -> Tuple of n, NAT means :Def5: :: RADIX_2:def 5
for i being Nat st i in Seg n holds
it . i = DigitDC2 (x,i,k);

existence
ex b₁ being Tuple of n, NAT st
for i being Nat st i in Seg n holds
b₁ . i = DigitDC2 (x,i,k)

proof end;

uniqueness
for b₁, b₂ being Tuple of n, NAT st ( for i being Nat st i in Seg n holds
b₁ . i = DigitDC2 (x,i,k) ) & ( for i being Nat st i in Seg n holds
b₂ . i = DigitDC2 (x,i,k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines DecSD2 RADIX_2:def 5 :
for k, n, x being Nat
for b₄ being Tuple of n, NAT holds
( b₄ = DecSD2 (x,n,k) iff for i being Nat st i in Seg n holds
b₄ . i = DigitDC2 (x,i,k) );

theorem Th12: :: RADIX_2:12

for n, k being Nat
for x being Tuple of n, NAT
for y being Tuple of n,k -SD st x = y holds
DigitSD2 (x,k) = DigitSD y

proof end;

theorem Th13: :: RADIX_2:13

for n, k being Nat
for x being Tuple of n, NAT
for y being Tuple of n,k -SD st x = y holds
SDDec2 (x,k) = SDDec y

proof end;

theorem Th14: :: RADIX_2:14

for x, n, k being Nat holds DecSD2 (x,n,k) = DecSD (x,n,k)

proof end;

theorem Th15: :: RADIX_2:15

for n being Nat st n >= 1 holds
for m, k being Nat st m is_represented_by n,k holds
m = SDDec2 ((DecSD2 (m,n,k)),k)

proof end;

:: radix-2^k SD numbers and its correctness

definition

let q be Integer;
let f, j, k, n be Nat;
let 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;

correctness
coherence
(q * (DigA (c,j))) mod f is Integer;
;

end;

:: deftheorem defines Table1 RADIX_2:def 6 :
for q being Integer
for f, j, k, n being Nat
for c being Tuple of n,k -SD holds Table1 (q,c,f,j) = (q * (DigA (c,j))) mod f;

definition

let q be Integer;
let k, f, n be Nat;
let c be Tuple of n,k -SD ;
assume A1: n >= 1 ;

func Mul_mod (q,c,f,k) -> Tuple of n, INT means :Def7: :: RADIX_2:def 7
( it . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = it . i & I2 = it . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) );

existence
ex b₁ being Tuple of n, INT st
( b₁ . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b₁ . i & I2 = b₁ . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) )

proof end;

uniqueness
for b₁, b₂ being Tuple of n, INT st b₁ . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b₁ . i & I2 = b₁ . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) & b₂ . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b₂ . i & I2 = b₂ . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines Mul_mod RADIX_2:def 7 :
for q being Integer
for k, f, n being Nat
for c being Tuple of n,k -SD st n >= 1 holds
for b₆ being Tuple of n, INT holds
( b₆ = Mul_mod (q,c,f,k) iff ( b₆ . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b₆ . i & I2 = b₆ . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) ) );

theorem :: RADIX_2:16

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

proof end;

:: radix-2^k SD numbers and its correctness

definition

let n, f, j, m be Nat;
let e be Tuple of n, NAT ;

func Table2 (m,e,f,j) -> Element of NAT equals :: RADIX_2:def 8
(m |^ (e /. j)) mod f;

correctness
coherence
(m |^ (e /. j)) mod f is Element of NAT ;
;

end;

:: deftheorem defines Table2 RADIX_2:def 8 :
for n, f, j, m being Nat
for e being Tuple of n, NAT holds Table2 (m,e,f,j) = (m |^ (e /. j)) mod f;

definition

let k, f, m, n be Nat;
let e be Tuple of n, NAT ;
assume A1: n >= 1 ;

func Pow_mod (m,e,f,k) -> Tuple of n, NAT means :Def9: :: RADIX_2:def 9
( it . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = it . i & i2 = it . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) );

existence
ex b₁ being Tuple of n, NAT st
( b₁ . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b₁ . i & i2 = b₁ . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) )

proof end;

uniqueness
for b₁, b₂ being Tuple of n, NAT st b₁ . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b₁ . i & i2 = b₁ . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) & b₂ . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b₂ . i & i2 = b₂ . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines Pow_mod RADIX_2:def 9 :
for k, f, m, n being Nat
for e being Tuple of n, NAT st n >= 1 holds
for b₆ being Tuple of n, NAT holds
( b₆ = Pow_mod (m,e,f,k) iff ( b₆ . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b₆ . i & i2 = b₆ . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) ) );

theorem :: RADIX_2:17

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

proof end;