Code

Word eval refactor#1136

Code

Merged

robdockins merged 46 commits intomasterGaloisInc/cryptol:masterfrom word-eval-refactorGaloisInc/cryptol:word-eval-refactorCopy head branch name to clipboardApr 14, 2021

+1,939-1,739

Commits

Commits on Apr 13, 2021

• Refactor the VWord constructor and WordValue type.

  Show description for 1377fc9
  robdockins

  committed
  1377fc9

• Remove obsolete functions

  robdockins

  committed
  d4e5fc2

• Rework the # operator.

  Show description for 3942a3d
  robdockins

  committed
  3942a3d

• Remove the eta delay mechanisim from the evaluator.

  Show description for b24e2f5
  robdockins

  committed
  b24e2f5

• Squash warnings

  robdockins

  committed
  5a84ea5

• Break SeqMap out into a separate module

  robdockins

  committed
  3f71046

• Relocate most of the logic that works directly on WordValue values

  Show description for b9635b2
  robdockins

  committed
  b9635b2

• Complete the process of making WordVal abstract.

  robdockins

  committed
  7fc748d

• Move WordValue into a separate module.

  robdockins

  committed
  3f18544

• Complete the job of making SeqMap abstract.

  robdockins

  committed
  87d8912

• Update cryptol-remote-api

  robdockins

  committed
  a112ed8

• Make take and drop primitive instead of splitAt.

  Show description for d3accfb
  robdockins

  committed
  d3accfb

• Fix test suite

  robdockins

  committed
  b5454bc

• Tweak split, join, reverse and transpose.

  Show description for 5011771
  robdockins

  committed
  5011771

• Update the reference interpreter

  robdockins

  committed
  69a589d

• Remove uses of panic in SeqMap

  robdockins

  committed
  6bf4d2e

• Continue consolidating WordValue code into the related module

  robdockins

  committed
  a2aa432

• Consolidate some code related to indexing and shifting.

  Show description for ebc8327
  robdockins

  committed
  ebc8327

• Reduce the amount of sequence memoization that occurs in shifts.

  Show description for 8ca536d
  robdockins

  committed
  8ca536d

• Rework shifting in the concrete simulator to use the same code paths

  Show description for d291318
  robdockins

  committed
  d291318

• Make indexPrim lazier in its sequence argument.

  robdockins

  committed
  07f4ba9

• Fix import in cryptol-remote-api

  robdockins

  committed
  e7df405

• Push word shifts into the Backend class and define shifts uniformly.

  robdockins

  committed
  9d41839

• Implement signed right shift uniformly

  robdockins

  committed
  7c3f1ac

• Make word updates more uniform between SBV and What4.

  Show description for f88b67d
  robdockins

  committed
  f88b67d

• Try harder to see if thunks have already been forced.

  robdockins

  committed
  afd4cd6

• typo

  robdockins

  committed
  9823884

• Fix a bug with width accounting

  robdockins

  committed
  62bcaba

• Fix another width accounting bug

  robdockins

  committed
  6d53e91

• Stop eta-expanding the error combinator.

  Show description for 55a48ba
  robdockins

  committed
  55a48ba

• Change largeBitsVal into bitmapWordVal.

  Show description for e65bf8c
  robdockins

  committed
  e65bf8c

• Temporary fix to the test for issue211.

  Show description for b812cd5
  robdockins

  committed
  b812cd5

• Update reference implementation and documentation

  robdockins

  committed
  cc8822f

• Remove the splitWordVal operation.

  Show description for 149428c
  robdockins

  committed
  149428c

• Tweak the way delayWordValue works.

  Show description for 5f4b979
  robdockins

  committed
  5f4b979

• Don't reexport the SeqMap API

  robdockins

  committed
  6853ba0

• Keep a thunk for packed words alongside bitmap representations.

  Show description for f7d66df
  robdockins

  committed
  f7d66df

• Make joinWordVal lazier in its arguments.

  robdockins

  committed
  77f6718

• Increase the strictness in the SuiteB SHA padding function.

  Show description for 5d96829
  robdockins

  committed
  5d96829

• Make joinWords lazier in its arguments

  robdockins

  committed
  d4c3402

• Make the "large bit size" a bit more reasonable.

  robdockins

  committed
  838a252

• Update the test for issue 211 to restore the old test behavior.

  Show description for 31ab387
  robdockins

  committed
  31ab387

• Add test case for issue640

  Show description for 69ad34b
  robdockins

  committed
  69ad34b

• Fix test suite

  robdockins

  committed
  aac42f4

• Fixes that help a small amount with space leaks

  robdockins

  committed
  29c5bc9

• Rework memoMap to squash space leaks.

  Show description for 3f66dbf
  robdockins

  committed
  3f66dbf