Code

Tactics for serialize#549

Code

Merged

karthikbhargavan merged 20 commits intodevcryspen/libcrux:devfrom lf-tactics-serializecryspen/libcrux:lf-tactics-serializeCopy head branch name to clipboardAug 31, 2024

+2,029-75

Commits

Commits on Aug 30, 2024

• Update and improve Makefiles

  W95Psp

  committed
  e46edf3

  Copy full SHA for e46edf3

• Reintroduce BitVecEq from previous proofs

  W95Psp

  committed
  0fb14cb

  Copy full SHA for 0fb14cb

• intro tactic library to do hybrid norm/rewrite inside terms

  W95Psp

  committed
  8feb781

  Copy full SHA for 8feb781

• Kill let mut, use array literal instead

  W95Psp

  committed
  47177fe

  Copy full SHA for 47177fe

• Serialization pre/post in vector/traits.rs + spec in *Math.fst

  W95Psp

  committed
  77fe334

  Copy full SHA for 77fe334

• gitignore

  W95Psp

  committed
  2e5a142

  Copy full SHA for 2e5a142

• intrinsics

  W95Psp

  committed
  ff0e6ad

  Copy full SHA for ff0e6ad

• partial proofs

  W95Psp

  committed
  bfeeda3

  Copy full SHA for bfeeda3

• avx2: serialize: manual proofs

  W95Psp

  committed
  7c4e54b

  Copy full SHA for 7c4e54b

• portable: serialize: manual proofs

  W95Psp

  committed
  dd063cc

  Copy full SHA for dd063cc

• makefile, more fixes

  W95Psp

  committed
  64a2732

  Copy full SHA for 64a2732

Commits on Aug 31, 2024

• Comment out pre/post-conditions for serialize fun in vector/traits.rs

  mamonet

  committed
  ea8f110

  Copy full SHA for ea8f110

• Fix return array in serialize_1

  mamonet

  committed
  c8b2d7e

  Copy full SHA for c8b2d7e

• Fix fstar::replace for mm256_srli_epi16

  mamonet

  committed
  3635503

  Copy full SHA for 3635503

• Update extracted F* files for intrinsics and ml-kem

  mamonet

  committed
  10b4615

  Copy full SHA for 10b4615

• wip

  karthikbhargavan

  committed
  89af067

  Copy full SHA for 89af067

• wip

  karthikbhargavan

  committed
  133225f

  Copy full SHA for 133225f

• verifying

  karthikbhargavan

  committed
  56eed0a

  Copy full SHA for 56eed0a

• fmt

  karthikbhargavan

  committed
  aa003c8

  Copy full SHA for aa003c8

• fstar feat

  karthikbhargavan

  committed
  87ab89d

  Copy full SHA for 87ab89d