Code

Saturated arithmetic experiment#1609

Code

Draft

andres-erbsen wants to merge 45 commits intomit-plv:mastermit-plv/fiat-crypto:masterfrom andres-erbsen:saturated-experimentandres-erbsen/fiat-crypto:saturated-experimentCopy head branch name to clipboard

+44,602-42,821

Commits

Commits on Aug 21, 2023

• WIP

  

  JasonGross

  authored and

  andres-erbsen

  committed
  b41ffbf

  Copy full SHA for b41ffbf

• WIP reworking value type

  

  JasonGross

  authored and

  andres-erbsen

  committed
  94eec46

  Copy full SHA for 94eec46

• WIP

  

  JasonGross

  authored and

  andres-erbsen

  committed
  2e49ffa

  Copy full SHA for 2e49ffa

• rewrite cmov c,0,-1 to sbb

  andres-erbsen

  committed
  187a6d7

  Copy full SHA for 187a6d7

• saturated non-canonical pseudo-Mersenne addition

  andres-erbsen

  committed
  1f7f336

  Copy full SHA for 1f7f336

• WIP before sub

  andres-erbsen

  committed
  a7c0485

  Copy full SHA for a7c0485

• bracketize eval_reduce3

  andres-erbsen

  committed
  e8c4417

  Copy full SHA for e8c4417

• reduce3 cleanup WIP

  andres-erbsen

  committed
  d7fcb74

  Copy full SHA for d7fcb74

• SolinasReduction cleanup WIP

  andres-erbsen

  committed
  60de154

  Copy full SHA for 60de154

• saturated_pseudomersenne_reduction_converges

  andres-erbsen

  committed
  40480e5

  Copy full SHA for 40480e5

• saturated_pseudomersenne_reduction_converges'

  andres-erbsen

  committed
  1fc5677

  Copy full SHA for 1fc5677

• example of needless substitution in DCE

  andres-erbsen

  committed
  b02ad58

  Copy full SHA for b02ad58

• WIP

  andres-erbsen

  committed
  598c717

  Copy full SHA for 598c717

• WIP

  andres-erbsen

  committed
  c37e376

  Copy full SHA for c37e376

• WIP

  andres-erbsen

  committed
  9c83da7

  Copy full SHA for 9c83da7

• WIP

  andres-erbsen

  committed
  4e69cce

  Copy full SHA for 4e69cce

• Compilers positive WIP

  andres-erbsen

  committed
  e60e284

  Copy full SHA for e60e284

• WIP Z reification fails

  andres-erbsen

  committed
  cca1d1c

  Copy full SHA for cca1d1c

• minor cleanup in eval

  andres-erbsen

  committed
  108e222

  Copy full SHA for 108e222

• eval_mul

  andres-erbsen

  committed
  7f6c4c3

  Copy full SHA for 7f6c4c3

• mulmod

  andres-erbsen

  committed
  e24dc54

  Copy full SHA for e24dc54

• eval_mulmod

  andres-erbsen

  committed
  85339a7

  Copy full SHA for 85339a7

• things kinda build now

  andres-erbsen

  committed
  32aa606

  Copy full SHA for 32aa606

• use positive

  andres-erbsen

  committed
  453d314

  Copy full SHA for 453d314

• cleanup

  andres-erbsen

  committed
  b522ee7

  Copy full SHA for b522ee7

• canon_correct

  andres-erbsen

  committed
  e847dc3

  Copy full SHA for e847dc3

• canon still does not reify

  andres-erbsen

  committed
  39dc6d9

  Copy full SHA for 39dc6d9

• hackily reify weight

  andres-erbsen

  committed
  d6a1bac

  Copy full SHA for d6a1bac

• divmodw

  andres-erbsen

  committed
  8881279

  Copy full SHA for 8881279

• prototype bounds-checked mul

  andres-erbsen

  committed
  1b6e43f

  Copy full SHA for 1b6e43f

• union bounds of conditionals

  andres-erbsen

  committed
  599ab30

  Copy full SHA for 599ab30

• fix build enough to see synthesis output

  andres-erbsen

  committed
  6492826

  Copy full SHA for 6492826

• genereate reasonable fe4_mul by iterating rw/bounds

  andres-erbsen

  committed
  e3dd69c

  Copy full SHA for e3dd69c

Commits on Aug 22, 2023

• dlet more

  andres-erbsen

  committed
  29da032

  Copy full SHA for 29da032

Commits on Aug 23, 2023

• start implementing interleaved Montgomery reduction

  andres-erbsen

  committed
  fb346d9

  Copy full SHA for fb346d9

• p256_mul draft

  andres-erbsen

  committed
  68ba51e

  Copy full SHA for 68ba51e

Commits on Sep 6, 2023

• p256 square

  andres-erbsen

  committed
  47f058a

  Copy full SHA for 47f058a

Commits on Sep 8, 2023

• refactor product_scan_ for p256 sqr bounds

  andres-erbsen

  committed
  0267d1b

  Copy full SHA for 0267d1b

Commits on Sep 19, 2023

• p256 square diagonal carry chain optimization

  andres-erbsen

  committed
  3d4d51d

  Copy full SHA for 3d4d51d

Commits on Sep 26, 2023

• p256_adx in CLI, not particularly clean

  andres-erbsen

  committed
  43a5e6a

  Copy full SHA for 43a5e6a

Commits on Sep 27, 2023

• condsub' instead of canon in p256_mul

  andres-erbsen

  committed
  2a6f73f

  Copy full SHA for 2a6f73f

Commits on Sep 29, 2023

• fill in some admits

  andres-erbsen

  committed
  dd405bb

  Copy full SHA for dd405bb

• fix p256_sqr Qed

  andres-erbsen

  committed
  b0c6b36

  Copy full SHA for b0c6b36

• clean up p256adx

  andres-erbsen

  committed
  0d69640

  Copy full SHA for 0d69640

• garbage-collect SlowPrimeSynthesisExamples

  andres-erbsen

  committed
  e6077db

  Copy full SHA for e6077db