Code

Bulk addition memory safety#66

Code

Merged

andreistefanescu merged 28 commits intomainGaloisInc/BLST-Verification:mainfrom bulk_addition_memory_safetyGaloisInc/BLST-Verification:bulk_addition_memory_safetyCopy head branch name to clipboardNov 8, 2021

+877-6

Commits

Commits on Aug 13, 2021

• add blst_bulk_addition submodule

  

  Giuliano Losa

  committed
  ea81bac

  Copy full SHA for ea81bac

• mount blst_bulk_addition

  

  Giuliano Losa

  committed
  757fb5f

  Copy full SHA for 757fb5f

• build blst_bulk_addition

  

  Giuliano Losa

  committed
  9672214

  Copy full SHA for 9672214

• fix docker-compose.yml

  

  Giuliano Losa

  committed
  77ab8df

  Copy full SHA for 77ab8df

• add bulk_addition_memory_safety

  

  Giuliano Losa

  committed
  7b00d44

  Copy full SHA for 7b00d44

• first attempt at POINTonE1s_accumulate mem safety

  Show description for df66c7e
  

  Giuliano Losa

  committed
  df66c7e

  Copy full SHA for df66c7e

Commits on Aug 27, 2021

• make some progress

  

  Giuliano Losa

  committed
  bad7c38

  Copy full SHA for bad7c38

• another problem...

  

  Giuliano Losa

  committed
  9b72f76

  Copy full SHA for 9b72f76

• two cases of memory safety

  

  Giuliano Losa

  committed
  af6725b

  Copy full SHA for af6725b

• fix call parameter

  

  Giuliano Losa

  committed
  08817ca

  Copy full SHA for 08817ca

Commits on Aug 28, 2021

• add E2 cases

  

  Giuliano Losa

  committed
  8919c48

  Copy full SHA for 8919c48

Commits on Sep 15, 2021

• set do_prove to true

  

  Giuliano Losa

  committed
  47e25f6

  Copy full SHA for 47e25f6

Commits on Sep 16, 2021

• note that the interesting cases remain TODO

  

  Giuliano Losa

  committed
  812c4af

  Copy full SHA for 812c4af

Commits on Oct 1, 2021

• add overrides for internal functions

  Show description for 0d9b6ed
  

  Giuliano Losa

  committed
  0d9b6ed

  Copy full SHA for 0d9b6ed

• add mem safety for n=16 on E1

  

  Giuliano Losa

  committed
  a22d9ac

  Copy full SHA for a22d9ac

• add mem proof for n=17

  

  Giuliano Losa

  committed
  710d614

  Copy full SHA for 710d614

• add mem safety for n=3

  

  Giuliano Losa

  committed
  3d7f264

  Copy full SHA for 3d7f264

• use spec generated by python script

  

  Giuliano Losa

  committed
  484a6a7

  Copy full SHA for 484a6a7

Commits on Oct 2, 2021

• add mem safety proofs for more sizes (still E1)

  Show description for 5bef4a3
  

  Giuliano Losa

  committed
  5bef4a3

  Copy full SHA for 5bef4a3

• add second spec

  

  Giuliano Losa

  committed
  2dea585

  Copy full SHA for 2dea585

Commits on Oct 4, 2021

• remove overrides for accumulate

  

  Giuliano Losa

  committed
  785e033

  Copy full SHA for 785e033

Commits on Oct 5, 2021

• add E2 proofs

  

  Giuliano Losa

  committed
  b50fd2f

  Copy full SHA for b50fd2f

• fix build_x86

  

  Giuliano Losa

  committed
  670fa00

  Copy full SHA for 670fa00

• add exp2_for_bulk_add.saw

  

  Giuliano Losa

  committed
  033de44

  Copy full SHA for 033de44

Commits on Oct 12, 2021

• add bulk_add to ci

  

  Giuliano Losa

  committed
  9ef4e61

  Copy full SHA for 9ef4e61

• remove unused specs

  

  Giuliano Losa

  committed
  3d84f34

  Copy full SHA for 3d84f34

• add cryptol specs related to bulk addition

  

  Giuliano Losa

  committed
  8b01dce

  Copy full SHA for 8b01dce

• actually prove things

  

  Giuliano Losa

  committed
  3535a11

  Copy full SHA for 3535a11