Package montgomery-thm: Properties of Montgomery multiplication

Information

name	montgomery-thm
version	1.10
description	Properties of Montgomery multiplication
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2013-08-09
requires	bool montgomery-def natural
show	Data.Bool Number.Natural

Files

Package tarball montgomery-thm-1.10.tgz
Theory source file montgomery-thm.thy (included in the package tarball)

Defined Constants

HOLLight
- HOLLight.montgomery_comb
- HOLLight.montgomery_loop
- HOLLight.montgomery_sc
- HOLLight.montgomery_y

Theorems

⊦ ∀n r k a m. ¬(n = 0) ∧ n ≤ r ∧ a < r ⇒ Montgomery.doubleExp n r k a m < r

⊦ ∀n r k a.
¬(n = 0) ∧ ¬(r = 0) ∧ a ≤ r * r ⇒ Montgomery.reduce n r k a < r + n

⊦ ∀n r k m a.
¬(n = 0) ∧ ¬(r = 0) ∧ a ≤ r * m ⇒ Montgomery.reduce n r k a < m + n

⊦ ∀n r k a.
¬(n = 0) ∧ ¬(r = 0) ∧ a ≤ r * n ⇒ Montgomery.reduce n r k a < 2 * n

⊦ ∀n r s k a.
¬(n = 0) ∧ r * s = k * n + 1 ⇒
Montgomery.reduce n r k a mod n = a * s mod n

⊦ ∀n r s k a m.
¬(n = 0) ∧ n ≤ r ∧ r * s = k * n + 1 ⇒
Montgomery.doubleExp n r k a m mod n = (a * s) ↑ 2 ↑ m * r mod n

⊦ ∀ys yc ys' yc'.
    HOLLight.montgomery_y ys yc ys' yc' ⇔
    ∃r ys₀ yc₀ yc₁ ys0' ys1' yc0' yc1'.
      Hardware.Bus.width ys = r + 1 ∧ Hardware.Bus.width yc = r + 1 ∧
      Hardware.Bus.width ys' = r + 1 ∧ Hardware.Bus.width yc' = r + 1 ∧
      Hardware.Bus.sub ys 1 r ys₀ ∧ Hardware.Bus.sub yc 0 r yc₀ ∧
      Hardware.Bus.wire yc r yc₁ ∧ Hardware.Bus.sub ys' 0 r ys0' ∧
      Hardware.Bus.wire ys' r ys1' ∧ Hardware.Bus.sub yc' 0 r yc0' ∧
      Hardware.Bus.wire yc' r yc1' ∧
      Hardware.Bus.compressor2 ys₀ yc₀ ys0' yc0' ∧ ys1' = yc₁ ∧
      yc1' = Hardware.ground

⊦ ∀nb kb xs xc ys yc sa sb sx sy sz so ca cb ks kc ns nc ys' yc' sa' sb'
    sx' sy' sz' so' ca' cb' ks' kc' ns' nc' zs' zc'.
    HOLLight.montgomery_comb nb kb xs xc ys yc sa sb sx sy sz so ca cb ks
      kc ns nc ys' yc' sa' sb' sx' sy' sz' so' ca' cb' ks' kc' ns' nc' zs'
      zc' ⇔
    ∃ys₀.
      Hardware.Bus.wire ys 0 ys₀ ∧ HOLLight.montgomery_y ys yc ys' yc' ∧
      HOLLight.montgomery_sc xs xc ys₀ sa sb ca cb sa' sb' ca' cb'

⊦ ∀ld nb kb xs xc ys yc zs' zc'.
    HOLLight.montgomery_loop ld nb kb xs xc ys yc zs' zc' ⇔
    ∃r ysp ycp sap sbp sxp syp szp sop cap cbp ksp kcp nsp ncp ysq ycq saq
      sbq sxq syq szq soq caq cbq ksq kcq nsq ncq ysr ycr sar sbr sxr syr
      szr sor car cbr ksr kcr nsr ncr.
      Hardware.Bus.width nb = r ∧ Hardware.Bus.width kb = r ∧
      Hardware.Bus.width xs = r ∧ Hardware.Bus.width xc = r ∧
      Hardware.Bus.width ys = r ∧ Hardware.Bus.width yc = r ∧
      Hardware.Bus.width zs' = r ∧ Hardware.Bus.width zc' = r ∧
      HOLLight.montgomery_comb nb kb xs xc ysp ycp sap sbp sxp syp szp sop
        cap cbp ksp kcp nsp ncp ysq ycq saq sbq sxq syq szq soq caq cbq ksq
        kcq nsq ncq zs' zc' ∧ Hardware.Bus.case1 ld ys ysq ysr ∧
      Hardware.Bus.case1 ld yc ycq ycr ∧
      Hardware.Bus.case1 ld (Hardware.Bus.ground (r + 1)) saq sar ∧
      Hardware.Bus.case1 ld (Hardware.Bus.ground r) sbq sbr ∧
      Hardware.case1 ld Hardware.ground sxq sxr ∧
      Hardware.case1 ld Hardware.ground syq syr ∧
      Hardware.case1 ld Hardware.ground szq szr ∧
      Hardware.case1 ld Hardware.ground soq sor ∧
      Hardware.Bus.case1 ld (Hardware.Bus.ground r) caq car ∧
      Hardware.Bus.case1 ld (Hardware.Bus.ground r) cbq cbr ∧
      Hardware.Bus.case1 ld (Hardware.Bus.ground r) ksq ksr ∧
      Hardware.Bus.case1 ld (Hardware.Bus.ground r) kcq kcr ∧
      Hardware.Bus.case1 ld (Hardware.Bus.ground r) nsq nsr ∧
      Hardware.Bus.case1 ld (Hardware.Bus.ground r) nsq nsr ∧
      Hardware.Bus.delay ysr ysp ∧ Hardware.Bus.delay ycr ycp ∧
      Hardware.Bus.delay sar sap ∧ Hardware.Bus.delay sbr sbp ∧
      Hardware.delay sxr sxp ∧ Hardware.delay syr syp ∧
      Hardware.delay szr szp ∧ Hardware.delay sor sop ∧
      Hardware.Bus.delay car cap ∧ Hardware.Bus.delay cbr cbp ∧
      Hardware.Bus.delay ksr ksp ∧ Hardware.Bus.delay kcr kcp ∧
      Hardware.Bus.delay nsr nsp ∧ Hardware.Bus.delay ncr ncp

⊦ ∀xs xc ys₀ sa sb ca cb sa' sb' ca' cb'.
    HOLLight.montgomery_sc xs xc ys₀ sa sb ca cb sa' sb' ca' cb' ⇔
    ∃r sa₀ sa₁ sa₂ sb₀ sb₁ ca₀ ca₁ cb₀ cb₁ sa0' sa1' sa2' sb0' sb1' ca0'
      ca1' cb0' cb1' xsz xcz xsz₀ xsz₁ xcz₀ xcz₁.
      Hardware.Bus.width xs = r + 1 ∧ Hardware.Bus.width xc = r + 1 ∧
      Hardware.Bus.width sa = r + 2 ∧ Hardware.Bus.width sb = r + 1 ∧
      Hardware.Bus.width ca = r + 1 ∧ Hardware.Bus.width cb = r + 1 ∧
      Hardware.Bus.width sa' = r + 2 ∧ Hardware.Bus.width sb' = r + 1 ∧
      Hardware.Bus.width ca' = r + 1 ∧ Hardware.Bus.width cb' = r + 1 ∧
      Hardware.Bus.width xsz = r + 1 ∧ Hardware.Bus.width xcz = r + 1 ∧
      Hardware.Bus.wire sa 0 sa₀ ∧ Hardware.Bus.sub sa 1 r sa₁ ∧
      Hardware.Bus.wire sa (r + 1) sa₂ ∧ Hardware.Bus.wire sb 0 sb₀ ∧
      Hardware.Bus.sub sb 1 r sb₁ ∧ Hardware.Bus.wire ca 0 ca₀ ∧
      Hardware.Bus.sub ca 1 r ca₁ ∧ Hardware.Bus.sub cb 0 r cb₀ ∧
      Hardware.Bus.wire cb r cb₁ ∧ Hardware.Bus.wire sa' 0 sa0' ∧
      Hardware.Bus.sub sa' 1 r sa1' ∧ Hardware.Bus.wire sa' (r + 1) sa2' ∧
      Hardware.Bus.sub sb' 0 r sb0' ∧ Hardware.Bus.wire sb' r sb1' ∧
      Hardware.Bus.wire ca' 0 ca0' ∧ Hardware.Bus.sub ca' 1 r ca1' ∧
      Hardware.Bus.sub cb' 0 r cb0' ∧ Hardware.Bus.wire cb' r cb1' ∧
      Hardware.Bus.wire xsz 0 xsz₀ ∧ Hardware.Bus.sub xsz 1 r xsz₁ ∧
      Hardware.Bus.sub xcz 0 r xcz₀ ∧ Hardware.Bus.wire xcz r xcz₁ ∧
      Hardware.Bus.case1 ys₀ xs (Hardware.Bus.ground (r + 1)) xsz ∧
      Hardware.Bus.case1 ys₀ xc (Hardware.Bus.ground (r + 1)) xcz ∧
      Hardware.adder2 xsz₀ ca₀ sa0' ca0' ∧
      Hardware.Bus.compressor3 xsz₁ xcz₀ ca₁ sa1' ca1' ∧ sa2' = xcz₁ ∧
      Hardware.Bus.compressor3 sa₁ sb₁ cb₀ sb0' cb0' ∧
      Hardware.adder2 sa₂ cb₁ sb1' cb1'

External Type Operators

→
bool
Hardware
- Hardware.bus
- Hardware.wire
Number
- Natural
  - natural

External Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
Hardware
- Hardware.adder2
- Hardware.case1
- Hardware.delay
- Hardware.ground
- Bus
  - Hardware.Bus.case1
  - Hardware.Bus.compressor2
  - Hardware.Bus.compressor3
  - Hardware.Bus.delay
  - Hardware.Bus.ground
  - Hardware.Bus.sub
  - Hardware.Bus.width
  - Hardware.Bus.wire
Number
- Natural
  - *
  - +
  - -
  - <
  - ≤
  - ↑
  - bit0
  - bit1
  - div
  - mod
  - suc
  - zero
  - Montgomery
    - Montgomery.doubleExp
    - Montgomery.reduce

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ ∀t. t ⇒ t

⊦ ∀n. 0 ≤ n

⊦ ⊥ ⇔ ∀p. p

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ ⊥

⊦ ∀t. (∀x. t) ⇔ t

⊦ (∀) = λp. p = λx. ⊤

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ∧ ⊤ ⇔ t

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ∀t. t ∨ ⊤ ⇔ ⊤

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. 0 * n = 0

⊦ ∀n. 0 + n = n

⊦ ∀m. m + 0 = m

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

⊦ ∀m. m ↑ 0 = 1

⊦ ∀m. m * 1 = m

⊦ ∀n. n ↑ 1 = n

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀m. suc m = m + 1

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀m n. m * n = n * m

⊦ ∀m n. m + n = n + m

⊦ ∀n. n ↑ 2 = n * n

⊦ ∀n. 2 * n = n + n

⊦ ∀m n. ¬(m < n) ⇔ n ≤ m

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ ∀n. ¬(n = 0) ⇒ n mod n = 0

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀m n. m ↑ suc n = m * m ↑ n

⊦ ∀m n. ¬(n = 0) ⇒ m mod n < n

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀n r k a. Montgomery.doubleExp n r k a 0 = a

⊦ ∀m n. n ≤ m ⇒ m - n + n = m

⊦ ∀m n. m < n ⇔ m ≤ n ∧ ¬(m = n)

⊦ ∀m n. ¬(m = 0) ⇒ m * n mod m = 0

⊦ ∀x y z. x = y ∧ y = z ⇒ x = z

⊦ ∀m n p. m * (n * p) = m * n * p

⊦ ∀m n p. m ↑ (n * p) = (m ↑ n) ↑ p

⊦ ∀a b n. b < a * n ⇒ b div a < n

⊦ ∀m n p. m + n < m + p ⇔ n < p

⊦ ∀m n p. n + m < p + m ⇔ n < p

⊦ ∀m n p. n + m ≤ p + m ⇔ n ≤ p

⊦ ∀m n p. m < n ∧ n ≤ p ⇒ m < p

⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p

⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n

⊦ ∀n m. ¬(n = 0) ⇒ m mod n mod n = m mod n

⊦ ∀m n p. m * (n + p) = m * n + m * p

⊦ ∀m n. ¬(n = 0) ⇒ (m div n) * n + m mod n = m

⊦ ∀m n p. m * n ≤ m * p ⇔ m = 0 ∨ n ≤ p

⊦ ∀m n p. m * p ≤ n * p ⇔ m ≤ n ∨ p = 0

⊦ ∀m n p. m * p < n * p ⇔ m < n ∧ ¬(p = 0)

⊦ ∀m n p q. m = n + q * p ⇒ m mod p = n mod p

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)

⊦ ∀n m p. ¬(n = 0) ⇒ m * (p mod n) mod n = m * p mod n

⊦ ∀n m p. ¬(n = 0) ⇒ (m mod n) * p mod n = m * p mod n

⊦ ∀n m p. ¬(n = 0) ⇒ (m mod n) ↑ p mod n = m ↑ p mod n

⊦ ∀n r k a. Montgomery.reduce n r k a = (a + (a * k mod r) * n) div r

⊦ ∀n m p. ¬(n = 0) ⇒ (m mod n) * (p mod n) mod n = m * p mod n

⊦ ∀n a b. ¬(n = 0) ⇒ (a mod n + b mod n) mod n = (a + b) mod n

⊦ ∀n r k a m.
    Montgomery.doubleExp n r k a (suc m) =
    let b ← Montgomery.reduce n r k (a * a) in
    let c ← if r ≤ b then b - n else b in
    Montgomery.doubleExp n r k c m