Code

More work on Montgomery#322

Code

Merged

JasonGross merged 7 commits intomastermit-plv/fiat-crypto:masterfrom fancymit-plv/fiat-crypto:fancyCopy head branch name to clipboardMar 7, 2018

+361-141

Commits

Commits on Feb 27, 2018

• factor out convert-mul-convert and prove correctness

  jadephilipoom

  committed
  5f55b86

  Copy full SHA for 5f55b86

Commits on Feb 28, 2018

• Add a dummy length argument to make partial evaluation work (see #321) and fixed up Montgomery notations

  jadephilipoom

  committed
  cde249a

  Copy full SHA for cde249a

• remove unneeded, commented-out code

  jadephilipoom

  committed
  37e6cb5

  Copy full SHA for 37e6cb5

• remove special-case convert-mul-convert implementation and use generalized one in Montgomery example

  jadephilipoom

  committed
  23129d1

  Copy full SHA for 23129d1

• make Montgomery do associational carries in a generalized way

  jadephilipoom

  committed
  5cf04c5

  Copy full SHA for 5cf04c5

• fix a typo, some comments, and notations

  jadephilipoom

  committed
  ce1dbc6

  Copy full SHA for ce1dbc6

Commits on Mar 1, 2018

• actually reprint montgomery and uncomment a couple notations -- should have been in last commit

  jadephilipoom

  committed
  fd168bc

  Copy full SHA for fd168bc