Code

Sparse bytes lemmas#659

Code

Open

virgil-serbanuta wants to merge 11 commits intomasterruntimeverification/wasm-semantics:masterfrom sparse-bytes-lemmasruntimeverification/wasm-semantics:sparse-bytes-lemmasCopy head branch name to clipboard

+2,783-57

Commits

Commits on Jun 26, 2024

• Disable replaceAtB for symbolic inputs

  virgil-serbanuta

  committed
  7e908d3

• Add SparseBytes lemmas

  virgil-serbanuta

  committed
  4dcf8f6

• Set Version: 0.1.71

  

  devops

  committed
  ff07664

Commits on Jun 28, 2024

• Fix shift definedness

  virgil-serbanuta

  committed
  437e7f6

• Fix right shifting of negative numbers: -1 >>Int 1 ==K -1

  virgil-serbanuta

  committed
  8a3e183

• Fix lemmas

  virgil-serbanuta

  committed
  204e055

• Use total versions of operators.

  virgil-serbanuta

  committed
  3bca8d7

• Enable trivial evaluation for extractSparseBytes

  virgil-serbanuta

  committed
  7d71631

• Int simplification lemmas

  virgil-serbanuta

  committed
  8b17c66

• Merge branch 'master' into sparse-bytes-lemmas

  virgil-serbanuta

  authored
  22d891a

Commits on Aug 7, 2024

• Set Version: 0.1.74

  

  devops

  authored and

  gtrepta

  committed
  46d9252