Reservoir

No results found
All Packages

remco-mulv0.1.0

#math
  • Readme
  • Versions (1)
  • Dependencies (8)

Verification of Remco's full 256x256 bit multiplication

This repo attempts to verify Remco's widely used mulDiv function.

At the moment it only verifies that the computation of the upper 256 bits of the 512 bit product via sub(sub(x1, x0), lt(x1, x0)) is verified.

Furthermore it verifies a specialization of fullMulDiv where the denominator is fixed to 2^128.

Credit to Remco Bloemen under MIT license: 2π.com/17/chinese-remainder-theorem/

  • MIT
  • 6 months ago
    Last updated on November 26, 2024 at 8:43:18PM
  • 9 stars

Lean

  • Commit 9f3241a (latest) builds on the old leanprover/lean4:v4.14.0-rc3
    v4.14.0-rc3
  • Commit 9f3241a (latest) builds on the old leanprover/lean4:v4.14.0-rc2
    v4.14.0-rc2
  • Commit 9f3241a (latest) builds on the old leanprover/lean4:v4.13.0
    v4.13.0
  • Commit 46fb498 builds on the old leanprover/lean4:v4.13.0-rc4
    v4.13.0-rc4
  • Commit 9f3241a (latest) builds on its old leanprover/lean4:v4.13.0-rc3
    v4.13.0-rc3
  • 17 more

Repository

Philogy/remco-mul-verification

About

  • lean-lang.org
  • The Lean FRO
  • Terms of Use
  • Privacy Policy

Explore

  • Games
  • Playground
  • Community
  • Moogle
  • Loogle

Learn

  • The Lean Manual
  • Theorem Proving in Lean
  • Functional Programming in Lean
  • Mathematics in Lean
  • The Mechanics of Proof
  • How To Prove It With Lean

Social

  • leanprover
  • @leanprover
  • Lean FRO
  • leanprover