Code

Bounded integers#642

Code

Merged

W95Psp merged 12 commits intomaincryspen/hax:mainfrom bounded-integerscryspen/hax:bounded-integersCopy head branch name to clipboardMay 6, 2024

+1,396-221

Commits

Commits on May 6, 2024

• refactor(refinement-types): check instead of refine

  W95Psp

  committed
  730a133

  Copy full SHA for 730a133

• feat(hax-bounded-integers): intro

  W95Psp

  committed
  978e2c5

  Copy full SHA for 978e2c5

• feat(bounded-ints): derive Index and IndexMut for BoundedUsize

  W95Psp

  committed
  167d25c

  Copy full SHA for 167d25c

• feat(refinement-types): add invariant method to Refinement trait

  W95Psp

  committed
  1c76d2c

  Copy full SHA for 1c76d2c

• feat(refinement-types): intro. run-time check, intro. no_debug_assert flag

  W95Psp

  committed
  3ee7c60

  Copy full SHA for 3ee7c60

• feat(bounded-ints): check in extraction

  W95Psp

  committed
  22174cf

  Copy full SHA for 22174cf

• refactor(chacha20): use bounded ints

  W95Psp

  committed
  61c6250

  Copy full SHA for 61c6250

• feat(hax-lib): instances for refined ints

  W95Psp

  committed
  ebf04c8

  Copy full SHA for ebf04c8

• typo: no_assert_debug -> no_debug_runtime_check

  W95Psp

  committed
  33d9e72

  Copy full SHA for 33d9e72

• fix(chacha20): move hax-bounded-integers to the right workspace

  W95Psp

  committed
  b2602e0

  Copy full SHA for b2602e0

• feat: Makefiles: find include dirs via cargo metadata

  W95Psp

  committed
  46b3eca

  Copy full SHA for 46b3eca

• refactor(refinements): rename check to into_checked

  W95Psp

  committed
  d67383d

  Copy full SHA for d67383d