• All Packages
  • Criteria
    • All Packages
    • Criteria
  • Readme
  • Versions (1)
  • Dependencies (8)

Philogyremco-mul0.1.0

#math

METADATA

  • MIT
  • 9 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
  • 25 more

REPOSITORY

Philogy/remco-mul-verification

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/

Get Started

  • Install
  • Learn
  • Community
  • Reservoir

Documentation

  • Language reference
  • Lean API
  • Use cases
  • Cite Lean

Resources

  • Lean playground
  • VS Code extension
  • Loogle
  • Mathlib

FRO

  • Mission
  • Team
  • Roadmap
  • Contact

Policies

  • Privacy Policy
  • Terms of Use
© 2025 Lean FRO. All rights reserved.