Package montgomery-hardware: Hardware Montgomery multiplication

Information

Files

• Package tarball montgomery-hardware-1.0.tgz
• Theory source file montgomery-hardware.thy (included in the package tarball)

Defined Constants

• Hardware
  • Montgomery
    • Montgomery.doubleExp
    • Montgomery.multiply
      • Montgomery.multiply.compress
      • Montgomery.multiply.reduce

Theorems

⊦ ∀ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc jb d₃ d₄ rx ry rz dn zs zc t.
    signal ld t ∧
    Montgomery.multiply ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc jb d₃ d₄ rx ry
      rz dn zs zc ⇒ ¬signal dn t

⊦ ∀r ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc jb d₃ d₄ rx ry rz dn zs zc t k.
    Bus.width xs = r ∧ d₃ ≤ d₀ + (d₁ + (d₂ + (r + 1))) ∧
    (∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.toNatural (Bus.signal jb t) + (d₀ + (d₁ + (d₂ + (r + 3)))) =
    2 ↑ Bus.width jb + (Bus.width jb + d₃) ∧
    Montgomery.multiply ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc jb d₃ d₄ rx ry
      rz dn zs zc ⇒
    (signal dn (t + k) ⇔ d₃ + k = d₀ + (d₁ + (d₂ + (r + 2))))

⊦ ∀n r x xs xc d rx ry rz ys yc t.
    Bus.width rx = r ∧ ¬(n = 0) ∧ Bits.width x ≤ r + 2 ∧
    Bits.toNatural (Bus.signal xs t) +
    2 * Bits.toNatural (Bus.signal xc t) = x ∧
    Bus.signal xs (t + d) = Bus.signal xs t ∧
    Bus.signal xc (t + d) = Bus.signal xc t ∧
    Bits.toNatural (Bus.signal rx (t + d)) = 2 ↑ r mod n ∧
    Bits.toNatural (Bus.signal ry (t + d)) = 2 * 2 ↑ r mod n ∧
    Bits.toNatural (Bus.signal rz (t + d)) = 3 * 2 ↑ r mod n ∧
    Montgomery.multiply.compress xs xc d rx ry rz ys yc ⇒
    (Bits.toNatural (Bus.signal ys (t + d)) +
     2 * Bits.toNatural (Bus.signal yc (t + d))) mod n = x mod n

⊦ ∀n r k x y ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc zs zc t.
    Bus.width xs = r ∧ ¬(n = 0) ∧ Bits.width n ≤ r ∧
    Bits.toNatural (Bus.signal xs t) +
    2 * Bits.toNatural (Bus.signal xc t) = x ∧
    (∀i.
       d₀ ≤ i ∧ i ≤ d₀ + (r + 1) ⇒
       Bits.toNatural (Bus.signal ys (t + i)) +
       2 * Bits.toNatural (Bus.signal yc (t + i)) = y) ∧
    Montgomery.multiply.reduce ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc zs zc ⇒
    Bits.width x ≤ r + 2 ∧ Bits.width y ≤ r + 2 ∧
    Bits.width (x * y) ≤ r + 2 + (r + 2) ∧
    Bits.width (Montgomery.reduce n (2 ↑ (r + 2)) k (x * y)) ≤ r + 2

⊦ ∀xs xc d rx ry rz ys yc.
    Montgomery.multiply.compress xs xc d rx ry rz ys yc ⇔
    ∃r nct ns nc nsd ncd rnl rnh rn xs₀ xs₁ xs₂ xc₀ xc₁ xc₂ ys₀ ys₁ yc₀ yc₁
      rn₀ rn₁.
      Bus.width xs = r + 2 ∧ Bus.width xc = r + 2 ∧ Bus.width rx = r + 1 ∧
      Bus.width ry = r + 1 ∧ Bus.width rz = r + 1 ∧ Bus.width ys = r + 1 ∧
      Bus.width yc = r + 1 ∧ Bus.width rnl = r + 1 ∧
      Bus.width rnh = r + 1 ∧ Bus.width rn = r + 1 ∧ Bus.wire xs 0 xs₀ ∧
      Bus.sub xs 1 r xs₁ ∧ Bus.wire xs (r + 1) xs₂ ∧ Bus.sub xc 0 r xc₀ ∧
      Bus.wire xc r xc₁ ∧ Bus.wire xc (r + 1) xc₂ ∧ Bus.wire ys 0 ys₀ ∧
      Bus.sub ys 1 r ys₁ ∧ Bus.wire yc 0 yc₀ ∧ Bus.sub yc 1 r yc₁ ∧
      Bus.wire rn 0 rn₀ ∧ Bus.sub rn 1 r rn₁ ∧ adder2 xs₂ xc₁ ns nct ∧
      or2 nct xc₂ nc ∧ pipe ns d nsd ∧ pipe nc d ncd ∧
      Bus.case1 nsd rx (Bus.ground (r + 1)) rnl ∧ Bus.case1 nsd rz ry rnh ∧
      Bus.case1 ncd rnh rnl rn ∧ adder2 xs₀ rn₀ ys₀ yc₀ ∧
      Bus.adder3 xs₁ xc₀ rn₁ ys₁ yc₁

⊦ ∀ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc jb d₃ d₄ rx ry rz dn zs zc.
    Montgomery.multiply ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc jb d₃ d₄ rx ry
      rz dn zs zc ⇔
    ∃r jp jpd ps pc qsp qcp qsr qcr.
      Bus.width xs = r + 1 ∧ Bus.width xc = r + 1 ∧ Bus.width ys = r + 1 ∧
      Bus.width yc = r + 1 ∧ Bus.width ks = r + 2 ∧ Bus.width kc = r + 2 ∧
      Bus.width ns = r ∧ Bus.width nc = r ∧ Bus.width rx = r + 1 ∧
      Bus.width ry = r + 1 ∧ Bus.width rz = r + 1 ∧ Bus.width zs = r + 1 ∧
      Bus.width zc = r + 1 ∧ Bus.width ps = r + 2 ∧ Bus.width pc = r + 2 ∧
      Bus.width qsp = r + 2 ∧ Bus.width qcp = r + 2 ∧
      Bus.width qsr = r + 2 ∧ Bus.width qcr = r + 2 ∧
      Montgomery.multiply.reduce ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc ps
        pc ∧ counterPulse ld jb jp ∧ pipe jp d₃ jpd ∧
      Bus.case1 jpd ps qsp qsr ∧ Bus.case1 jpd pc qcp qcr ∧ connect jp dn ∧
      Montgomery.multiply.compress qsp qcp d₄ rx ry rz zs zc ∧
      Bus.delay qsr qsp ∧ Bus.delay qcr qcp

⊦ ∀n r s k x y ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc zs zc t.
    Bus.width xs = r ∧ ¬(n = 0) ∧ Bits.width n ≤ r ∧
    2 ↑ (r + 2) * s = k * n + 1 ∧
    (∀i. i ≤ d₁ + (d₂ + (r + 1)) ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.toNatural (Bus.signal xs t) +
    2 * Bits.toNatural (Bus.signal xc t) = x ∧
    (∀i.
       d₀ ≤ i ∧ i ≤ d₀ + (r + 1) ⇒
       Bits.toNatural (Bus.signal ys (t + i)) +
       2 * Bits.toNatural (Bus.signal yc (t + i)) = y) ∧
    (∀i.
       d₀ + d₁ ≤ i ∧ i ≤ d₀ + (d₁ + (r + 1)) ⇒
       Bits.toNatural (Bus.signal ks (t + i)) +
       2 * Bits.toNatural (Bus.signal kc (t + i)) = k) ∧
    (∀i.
       d₀ + (d₁ + d₂) ≤ i ∧ i ≤ d₀ + (d₁ + (d₂ + (r + 1))) ⇒
       Bits.toNatural (Bus.signal ns (t + i)) +
       2 * Bits.toNatural (Bus.signal nc (t + i)) = n) ∧
    Montgomery.multiply.reduce ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc zs zc ⇒
    Bits.toNatural (Bus.signal zs (t + (d₀ + (d₁ + (d₂ + (r + 2)))))) +
    2 * Bits.toNatural (Bus.signal zc (t + (d₀ + (d₁ + (d₂ + (r + 2)))))) =
    Montgomery.reduce n (2 ↑ (r + 2)) k (x * y)

⊦ ∀ld mb xs xc d₀ d₁ ks kc d₂ ns nc jb d₃ d₄ rx ry rz dn ys yc.
    Montgomery.doubleExp ld mb xs xc d₀ d₁ ks kc d₂ ns nc jb d₃ d₄ rx ry rz
      dn ys yc ⇔
    ∃r sa sb jp ps pc qs qc sad sadd san sap saq sar sbd sbdd sbp sbq sbr
      srdd jpn psq psr pcq pcr md mdn.
      Bus.width xs = r + 1 ∧ Bus.width xc = r + 1 ∧ Bus.width ks = r + 2 ∧
      Bus.width kc = r + 2 ∧ Bus.width ns = r ∧ Bus.width nc = r ∧
      Bus.width rx = r + 1 ∧ Bus.width ry = r + 1 ∧ Bus.width rz = r + 1 ∧
      Bus.width ys = r + 1 ∧ Bus.width yc = r + 1 ∧ Bus.width ps = r + 1 ∧
      Bus.width pc = r + 1 ∧ Bus.width qs = r + 1 ∧ Bus.width qc = r + 1 ∧
      Bus.width psq = r + 1 ∧ Bus.width psr = r + 1 ∧
      Bus.width pcq = r + 1 ∧ Bus.width pcr = r + 1 ∧ not jp jpn ∧
      not md mdn ∧ not sa san ∧ and2 sb jp sap ∧ and2 san sap saq ∧
      or2 ld saq sar ∧ and2 sa mdn sbp ∧ case1 sb jpn sbp sbq ∧
      or2 ld sbq sbr ∧ pipe sa (d₃ + d₄) sad ∧ delay sad sadd ∧
      pipe sb (d₃ + d₄) sbd ∧ delay sbd sbdd ∧ and2 sadd sbdd srdd ∧
      eventCounter srdd mb sadd md ∧
      Montgomery.multiply sadd ps pc d₀ ps pc d₁ ks kc d₂ ns nc jb d₃ d₄ rx
        ry rz jp qs qc ∧ Bus.case1 sbd xs qs psq ∧
      Bus.case1 sad psq ps psr ∧ Bus.case1 sbd xc qc pcq ∧
      Bus.case1 sad pcq pc pcr ∧ nor2 sad sbd dn ∧ Bus.connect ps ys ∧
      Bus.connect pc yc ∧ delay sar sa ∧ delay sbr sb ∧ Bus.delay psr ps ∧
      Bus.delay pcr pc

⊦ ∀n r s k x y ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc jb d₃ d₄ rx ry rz dn zs
    zc t.
    Bus.width xs = r ∧ ¬(n = 0) ∧ Bits.width n ≤ r ∧
    2 ↑ (r + 2) * s = k * n + 1 ∧ d₃ ≤ d₀ + (d₁ + (d₂ + (r + 1))) ∧
    (∀i.
       i ≤ d₀ + (d₁ + (d₂ + (d₄ + (r + 2)))) ⇒
       (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.toNatural (Bus.signal xs t) +
    2 * Bits.toNatural (Bus.signal xc t) = x ∧
    (∀i.
       d₀ ≤ i ∧ i ≤ d₀ + (r + 1) ⇒
       Bits.toNatural (Bus.signal ys (t + i)) +
       2 * Bits.toNatural (Bus.signal yc (t + i)) = y) ∧
    (∀i.
       d₀ + d₁ ≤ i ∧ i ≤ d₀ + (d₁ + (r + 1)) ⇒
       Bits.toNatural (Bus.signal ks (t + i)) +
       2 * Bits.toNatural (Bus.signal kc (t + i)) = k) ∧
    (∀i.
       d₀ + (d₁ + d₂) ≤ i ∧ i ≤ d₀ + (d₁ + (d₂ + (r + 1))) ⇒
       Bits.toNatural (Bus.signal ns (t + i)) +
       2 * Bits.toNatural (Bus.signal nc (t + i)) = n) ∧
    Bits.toNatural (Bus.signal jb t) + (d₀ + (d₁ + (d₂ + (r + 3)))) =
    2 ↑ Bus.width jb + (Bus.width jb + d₃) ∧
    Bits.toNatural
      (Bus.signal rx (t + (d₀ + (d₁ + (d₂ + (d₄ + (r + 3))))))) =
    2 ↑ r mod n ∧
    Bits.toNatural
      (Bus.signal ry (t + (d₀ + (d₁ + (d₂ + (d₄ + (r + 3))))))) =
    2 * 2 ↑ r mod n ∧
    Bits.toNatural
      (Bus.signal rz (t + (d₀ + (d₁ + (d₂ + (d₄ + (r + 3))))))) =
    3 * 2 ↑ r mod n ∧
    Montgomery.multiply ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc jb d₃ d₄ rx ry
      rz dn zs zc ⇒
    (Bits.toNatural
       (Bus.signal zs (t + (d₀ + (d₁ + (d₂ + (d₄ + (r + 3))))))) +
     2 *
     Bits.toNatural
       (Bus.signal zc (t + (d₀ + (d₁ + (d₂ + (d₄ + (r + 3)))))))) mod n =
    x * y * s mod n

⊦ ∀n r s k m x ld mb xs xc d₀ d₁ ks kc d₂ ns nc jb d₃ d₄ rx ry rz dn ys yc
    t l.
    ∃d.
      ∀j.
        Bus.width xs = r ∧ Bits.width n ≤ r ∧ 2 ↑ (r + 2) * s = k * n + 1 ∧
        d₃ ≤ d₀ + (d₁ + (d₂ + (r + 1))) ∧ d₃ + (d₄ + 1) = l ∧
        Bus.width mb + l ≤ d₀ + (d₁ + (d₂ + (d₄ + (r + 4)))) ∧
        (∀i. i ≤ d + j ⇒ (signal ld (t + i) ⇔ i ≤ l)) ∧
        Bits.toNatural (Bus.signal mb (t + (l + (l + 1)))) + m =
        2 ↑ Bus.width mb + 1 ∧
        (Bits.toNatural (Bus.signal xs (t + (l + l))) +
         2 * Bits.toNatural (Bus.signal xc (t + (l + l)))) mod n =
        x * 2 ↑ (r + 2) mod n ∧
        (∀i.
           i < d ⇒
           Bits.toNatural (Bus.signal ks (t + (l + i))) +
           2 * Bits.toNatural (Bus.signal kc (t + (l + i))) = k) ∧
        (∀i.
           i < d ⇒
           Bits.toNatural (Bus.signal ns (t + (l + i))) +
           2 * Bits.toNatural (Bus.signal nc (t + (l + i))) = n) ∧
        (∀i.
           i < d ⇒
           Bits.toNatural (Bus.signal jb (t + (l + i))) +
           (d₀ + (d₁ + (d₂ + (r + 3)))) =
           2 ↑ Bus.width jb + (Bus.width jb + d₃)) ∧
        (∀i.
           i < d ⇒
           Bits.toNatural (Bus.signal rx (t + (l + i))) = 2 ↑ r mod n) ∧
        (∀i.
           i < d ⇒
           Bits.toNatural (Bus.signal ry (t + (l + i))) =
           2 * 2 ↑ r mod n) ∧
        (∀i.
           i < d ⇒
           Bits.toNatural (Bus.signal rz (t + (l + i))) =
           3 * 2 ↑ r mod n) ∧
        Montgomery.doubleExp ld mb xs xc d₀ d₁ ks kc d₂ ns nc jb d₃ d₄ rx
          ry rz dn ys yc ⇒
        (∀i. i ≤ d + j ⇒ (signal dn (t + (l + i)) ⇔ d ≤ i)) ∧
        (Bits.toNatural (Bus.signal ys (t + (l + (d + j)))) +
         2 * Bits.toNatural (Bus.signal yc (t + (l + (d + j))))) mod n =
        x ↑ 2 ↑ m * 2 ↑ (r + 2) mod n

⊦ ∀ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc zs zc.
    Montgomery.multiply.reduce ld xs xc d₀ ys yc d₁ ks kc d₂ ns nc zs zc ⇔
    ∃r pb ps pc pbp qb qs qc vb vs vc vt sa sb sc sd ms mc ld₁ ld₂ zs₀ zs₁
      zs₂ zc₀ zc₁ zc₂ zc₃ ps₀ pc₀ pb₁ pbp₀ pbp₁ qb₂ sa₀ sa₁ sa₂ sa₃ sa₄ sa₅
      sb₀ sb₁ sb₂ sd₀ sd₁ sd₂ sd₃ ms₀ ms₁ ms₂ ms₃ ms₄ mc₀ mc₁ mc₂ mc₃ mc₄
      mw.
      Bus.width xs = d₁ + (d₂ + (r + 2)) ∧
      Bus.width xc = d₁ + (d₂ + (r + 2)) ∧
      Bus.width ys = d₁ + (d₂ + (r + 2)) ∧
      Bus.width yc = d₁ + (d₂ + (r + 2)) ∧
      Bus.width ks = d₁ + (d₂ + (r + 3)) ∧
      Bus.width kc = d₁ + (d₂ + (r + 3)) ∧
      Bus.width ns = d₁ + (d₂ + (r + 1)) ∧
      Bus.width nc = d₁ + (d₂ + (r + 1)) ∧
      Bus.width zs = d₁ + (d₂ + (r + 3)) ∧
      Bus.width zc = d₁ + (d₂ + (r + 3)) ∧
      Bus.width ps = d₁ + (d₂ + (r + 2)) ∧
      Bus.width pc = d₁ + (d₂ + (r + 2)) ∧ Bus.width pbp = d₁ + (d₂ + 1) ∧
      Bus.width qs = d₁ + (d₂ + (r + 3)) ∧
      Bus.width qc = d₁ + (d₂ + (r + 3)) ∧
      Bus.width vs = d₁ + (d₂ + (r + 1)) ∧
      Bus.width vc = d₁ + (d₂ + (r + 1)) ∧
      Bus.width sa = d₁ + (d₂ + (r + 4)) ∧ Bus.width sb = r + 3 ∧
      Bus.width sc = d₁ + (d₂ + (r + 1)) ∧
      Bus.width sd = d₁ + (d₂ + (r + 2)) ∧
      Bus.width ms = d₁ + (d₂ + (r + 3)) ∧
      Bus.width mc = d₁ + (d₂ + (r + 3)) ∧
      Bus.sub zs 0 (d₁ + (d₂ + 1)) zs₀ ∧
      Bus.sub zs (d₁ + (d₂ + 1)) (r + 1) zs₁ ∧
      Bus.wire zs (d₁ + (d₂ + (r + 2))) zs₂ ∧ Bus.sub zc 0 (d₁ + d₂) zc₀ ∧
      Bus.wire zc (d₁ + d₂) zc₁ ∧ Bus.sub zc (d₁ + (d₂ + 1)) (r + 1) zc₂ ∧
      Bus.wire zc (d₁ + (d₂ + (r + 2))) zc₃ ∧ Bus.sub ps 0 (r + 4) ps₀ ∧
      Bus.sub pc 0 (r + 3) pc₀ ∧ Bus.wire pbp d₁ pb₁ ∧
      Bus.sub pbp 1 (d₁ + d₂) pbp₀ ∧ Bus.reverse pbp₀ pbp₁ ∧
      Bus.sub sa 0 (d₁ + d₂) sa₀ ∧ Bus.sub sa 0 (d₁ + (d₂ + (r + 1))) sa₁ ∧
      Bus.sub sa (d₁ + d₂) (r + 4) sa₂ ∧
      Bus.wire sa (d₁ + (d₂ + (r + 1))) sa₃ ∧
      Bus.wire sa (d₁ + (d₂ + (r + 2))) sa₄ ∧
      Bus.wire sa (d₁ + (d₂ + (r + 3))) sa₅ ∧ Bus.sub sb 0 (r + 1) sb₀ ∧
      Bus.wire sb (r + 1) sb₁ ∧ Bus.wire sb (r + 2) sb₂ ∧
      Bus.wire sd 0 sd₀ ∧ Bus.sub sd 0 (d₁ + (d₂ + (r + 1))) sd₁ ∧
      Bus.sub sd 1 (d₁ + (d₂ + (r + 1))) sd₂ ∧
      Bus.wire sd (d₁ + (d₂ + (r + 1))) sd₃ ∧
      Bus.sub ms 0 (d₁ + (d₂ + 1)) ms₀ ∧
      Bus.sub ms 0 (d₁ + (d₂ + (r + 1))) ms₁ ∧
      Bus.sub ms (d₁ + (d₂ + 1)) (r + 1) ms₄ ∧
      Bus.wire ms (d₁ + (d₂ + (r + 1))) ms₂ ∧
      Bus.wire ms (d₁ + (d₂ + (r + 2))) ms₃ ∧ Bus.sub mc 0 (d₁ + d₂) mc₀ ∧
      Bus.sub mc 0 (d₁ + (d₂ + (r + 1))) mc₁ ∧
      Bus.sub mc (d₁ + d₂) (r + 1) mc₂ ∧
      Bus.wire mc (d₁ + (d₂ + (r + 1))) mc₃ ∧
      Bus.wire mc (d₁ + (d₂ + (r + 2))) mc₄ ∧
      SumCarry.multiplier ld xs xc d₀ ys yc pb ps pc ∧
      pipe ld (d₀ + d₁) ld₁ ∧ Bus.pipe pb pbp ∧
      Bus.multiplier ld₁ pb₁ ks kc qb qs qc ∧ pipe ld₁ d₂ ld₂ ∧
      pipe qb d₂ qb₂ ∧ Bus.multiplier ld₂ qb₂ ns nc vb vs vc ∧
      sticky ld₂ vb vt ∧ Bus.connect pbp₁ sa₀ ∧
      Bus.adder3 sa₁ sc sd₁ ms₁ mc₁ ∧ adder2 sa₃ sd₃ ms₂ mc₃ ∧
      connect sa₄ ms₃ ∧ connect sa₅ mc₄ ∧ Bus.connect ms₀ zs₀ ∧
      Bus.connect mc₀ zc₀ ∧ connect ground zc₁ ∧
      Bus.adder3 sb₀ ms₄ mc₂ zs₁ zc₂ ∧ adder3 sb₁ ms₃ mc₃ zs₂ mw ∧
      or3 sb₂ mc₄ mw zc₃ ∧ Bus.delay ps₀ sa₂ ∧ Bus.delay pc₀ sb ∧
      Bus.delay vs sc ∧ delay vt sd₀ ∧ Bus.delay vc sd₂

External Type Operators

• →
• bool
• Data
  • List
    • list
• Hardware
  • bus
  • wire
• Number
  • Natural
    • natural
• Set
  • set

External Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ¬
    • cond
    • ⊥
    • ⊤
  • List
    • ::
    • length
• Hardware
  • adder2
  • adder3
  • and2
  • case1
  • connect
  • counterPulse
  • delay
  • eventCounter
  • ground
  • nor2
  • not
  • or2
  • or3
  • pipe
  • signal
  • sticky
  • xor2
  • Bus
    • Bus.adder3
    • Bus.append
    • Bus.case1
    • Bus.connect
    • Bus.delay
    • Bus.ground
    • Bus.multiplier
    • Bus.nil
    • Bus.pipe
    • Bus.reverse
    • Bus.signal
    • Bus.single
    • Bus.sub
    • Bus.width
    • Bus.wire
  • SumCarry
    • SumCarry.multiplier
• Number
  • Natural
    • *
    • +
    • <
    • ≤
    • ↑
    • bit0
    • bit1
    • div
    • fromBool
    • mod
    • suc
    • zero
    • Bits
      • Bits.bit
      • Bits.bound
      • Bits.cons
      • Bits.head
      • Bits.shiftLeft
      • Bits.shiftRight
      • Bits.tail
      • Bits.toNatural
      • Bits.width
    • Montgomery
      • Montgomery.reduce
• Set
  • ∅
  • disjoint
  • finite
  • fromPredicate
  • insert
  • ∩
  • ∈
  • size
  • ⊆
  • ∪

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ bit0 0 = 0

⊦ size ∅ = 0

⊦ ∀t. t ⇒ t

⊦ ∀n. 0 ≤ n

⊦ ∀n. n ≤ n

⊦ ⊥ ⇔ ∀p. p

⊦ fromPredicate (λx. ⊥) = ∅

⊦ ∀x. ¬(x ∈ ∅)

⊦ ∀t. t ∨ ¬t

⊦ ∀t. ¬signal ground t

⊦ ∀n. n < suc n

⊦ ∀n. n ≤ suc n

⊦ (¬) = λp. p ⇒ ⊥

⊦ ∀a. ∃x. x = a

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

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

⊦ ∀t. (λx. t x) = t

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

⊦ ∀t. ¬¬t ⇔ t

⊦ ∀t. (⊤ ⇔ t) ⇔ t

⊦ ∀t. (t ⇔ ⊤) ⇔ t

⊦ ∀t. ⊥ ∧ t ⇔ ⊥

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ∧ ⊥ ⇔ ⊥

⊦ ∀t. t ∧ ⊤ ⇔ t

⊦ ∀t. t ∧ t ⇔ t

⊦ ∀t. ⊥ ⇒ t ⇔ ⊤

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ ∀t. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ∀t. t ∨ ⊥ ⇔ t

⊦ ∀t. t ∨ ⊤ ⇔ ⊤

⊦ ∀t. t ∨ t ⇔ t

⊦ ∀x. Bus.append Bus.nil x = x

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. 0 * n = 0

⊦ ∀m. m * 0 = 0

⊦ ∀n. 0 + n = n

⊦ ∀m. m + 0 = m

⊦ ∀k. Bits.shiftLeft 0 k = 0

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

⊦ ∀w. Bus.width (Bus.single w) = 1

⊦ ∀n. bit1 n = suc (bit0 n)

⊦ ∀m. m ↑ 0 = 1

⊦ ∀m. m * 1 = m

⊦ ∀n. n ↑ 1 = n

⊦ ∀m. 1 * m = m

⊦ ∀m n. m ≤ m + n

⊦ ∀m n. n ≤ m + n

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

⊦ ∀x. size (insert x ∅) = 1

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀b. fromBool b = 0 ⇔ ¬b

⊦ ∀m. suc m = m + 1

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

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

⊦ ∀h t. Bits.head (Bits.cons h t) ⇔ h

⊦ ∀h t. Bits.tail (Bits.cons h t) = t

⊦ ∀b. fromBool b = if b then 1 else 0

⊦ ∀n. n < 2 ↑ Bits.width n

⊦ ∀n. 0 < n ⇔ ¬(n = 0)

⊦ ∀n. bit0 (suc n) = suc (suc (bit0 n))

⊦ ∀x y. x = y ⇔ y = x

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

⊦ ∀t₁ t₂. t₁ ∨ t₂ ⇔ t₂ ∨ t₁

⊦ ∀a b. (a ⇔ b) ⇒ a ⇒ b

⊦ ∀x t. length (Bus.signal x t) = Bus.width x

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

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

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

⊦ ∀n t. Bits.toNatural (Bus.signal (Bus.ground n) t) = 0

⊦ ∀n. 2 * n = n + n

⊦ ∀l. Bits.toNatural l < 2 ↑ length l

⊦ ∀n i. Bits.bit n i ⇔ Bits.head (Bits.shiftRight n i)

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

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

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

⊦ ∀m n. m < suc n ⇔ m ≤ n

⊦ ∀m n. suc m ≤ n ⇔ m < n

⊦ ∀m. m = 0 ∨ ∃n. m = suc n

⊦ ∀n. (∀i. ¬Bits.bit n i) ⇔ n = 0

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

⊦ ∀n. Bits.shiftLeft n 1 = 2 * n

⊦ ∀k. Bits.shiftLeft 1 k = 2 ↑ k

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

⊦ ∀p. ¬(∀x. p x) ⇔ ∃x. ¬p x

⊦ ∀p. ¬(∃x. p x) ⇔ ∀x. ¬p x

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

⊦ ∀x y. x ∈ insert y ∅ ⇔ x = y

⊦ ∀t₁ t₂. ¬t₁ ⇒ ¬t₂ ⇔ t₂ ⇒ t₁

⊦ ∀h t. Bits.toNatural (h :: t) = Bits.cons h (Bits.toNatural t)

⊦ ∀m n. m + suc n = suc (m + n)

⊦ ∀n k. Bits.shiftRight n (suc k) = Bits.tail (Bits.shiftRight n k)

⊦ ∀m n. suc m + n = suc (m + n)

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

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

⊦ ∀m n. suc m = suc n ⇔ m = n

⊦ ∀m n. suc m < suc n ⇔ m < n

⊦ ∀m n. suc m ≤ suc n ⇔ m ≤ n

⊦ ∀m n. m + n = m ⇔ n = 0

⊦ ∀m n. m + n = n ⇔ m = 0

⊦ ∀k n. Bits.shiftLeft n k = 0 ⇔ n = 0

⊦ ∀m n. m + n ≤ m ⇔ n = 0

⊦ ∀n k. Bits.bound (Bits.bound n k) k = Bits.bound n k

⊦ ∀s t. disjoint s t ⇔ s ∩ t = ∅

⊦ ∀s t. finite t ∧ s ⊆ t ⇒ finite s

⊦ ∀n. finite { m. m | m ≤ n }

⊦ ∀t₁ t₂. ¬(t₁ ∧ t₂) ⇔ ¬t₁ ∨ ¬t₂

⊦ ∀t₁ t₂. ¬(t₁ ∨ t₂) ⇔ ¬t₁ ∧ ¬t₂

⊦ ∀x y. Bus.sub x 0 (Bus.width x) y ⇔ y = x

⊦ ∀w t.
    Bits.toNatural (Bus.signal (Bus.single w) t) = fromBool (signal w t)

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

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

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

⊦ ∀m n. Bits.width (m * n) ≤ Bits.width m + Bits.width n

⊦ ∀n k. Bits.bound n k = n ⇔ Bits.width n ≤ k

⊦ ∀m n. m ≤ n ⇔ ∃d. n = m + d

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

⊦ ∀n k. Bits.shiftLeft n k = 2 ↑ k * n

⊦ ∀m n. m ≤ n ∧ n ≤ m ⇔ m = n

⊦ ∀n k. Bits.bound n k + Bits.shiftLeft (Bits.shiftRight n k) k = n

⊦ ∀m n. m < n ⇔ ∃d. n = m + suc d

⊦ ∀h t. Bits.cons h t = fromBool h + 2 * t

⊦ ∀p q. p ∨ (∃x. q x) ⇔ ∃x. p ∨ q x

⊦ ∀m n. m < suc n ⇔ m = n ∨ m < n

⊦ ∀n k. Bits.width n ≤ k ⇔ n < 2 ↑ k

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

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

⊦ ∀t₁ t₂ t₃. (t₁ ∧ t₂) ∧ t₃ ⇔ t₁ ∧ t₂ ∧ t₃

⊦ ∀t₁ t₂ t₃. (t₁ ∨ t₂) ∨ t₃ ⇔ t₁ ∨ t₂ ∨ t₃

⊦ ∀x y t. Bus.connect x y ⇒ Bus.signal y t = Bus.signal x t

⊦ ∀x y t. connect x y ⇒ (signal y t ⇔ signal x t)

⊦ ∀n k i. Bits.bit n (k + i) ⇔ Bits.bit (Bits.shiftRight n k) i

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

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

⊦ ∀n k₁ k₂.
    Bits.shiftLeft n (k₁ + k₂) = Bits.shiftLeft (Bits.shiftLeft n k₁) k₂