Commits

Branch selector

 master

User selector

All users

All time

Commit History

Commits on Jan 21, 2020

• Update README.md

  daejunpark

  authored
  86d4dca

  Copy full SHA for 86d4dca

• Update README.md

  daejunpark

  authored
  2236192

  Copy full SHA for 2236192

• Update README.md

  daejunpark

  committed
  7178783

  Copy full SHA for 7178783

Commits on Jan 18, 2020

• Update deposit-spec.ini.md

  daejunpark

  committed
  6603d82

  Copy full SHA for 6603d82

• add deposit-formal-verification.pdf

  daejunpark

  committed
  be618dd

  Copy full SHA for be618dd

Commits on Jan 17, 2020

• .k.rev: --concrete-rules in front-end (#307)

  denis-bogdanas

  authored
  cb2cb9a

  Copy full SHA for cb2cb9a

Commits on Jan 14, 2020

• Update deposit-spec.ini.md (#306)

  daejunpark

  authored
  349ffa5

  Copy full SHA for 349ffa5

Commits on Jan 11, 2020

• .k.rev: 2c9740fddcb2d0f52b59e5489e0a415e2ac3d3ce Improved simplification of equalities, for SOLAR. (#305)

  denis-bogdanas

  authored
  a57d3a6

  Copy full SHA for a57d3a6

• Migrating maintained ERC20 specs to full #buf (#299)

  Show description for 2608079
  denis-bogdanas

  authored
  2608079

  Copy full SHA for 2608079

Commits on Jan 10, 2020

• Removing #notKLabel from anywhere except gnosis/vyper gas computation (#292)

  Show description for 1092b58
  denis-bogdanas

  authored
  1092b58

  Copy full SHA for 1092b58

Commits on Dec 20, 2019

• .build/kevm.rev: updated to latest master. Including extension to kprove.mak to support concrete-rules.txt (#298)

  Show description for 3c14676
  denis-bogdanas

  authored
  3c14676

  Copy full SHA for 3c14676

• kprove.mak: generalized lemmas.k and local lemmas generation, required for Haskell. (#295)

  Show description for 5c7d327
  denis-bogdanas

  authored
  5c7d327

  Copy full SHA for 5c7d327

Commits on Dec 19, 2019

• Deposit (#293)

  Show description for e3c1ead
  daejunpark

  authored
  e3c1ead

  Copy full SHA for e3c1ead

Commits on Dec 11, 2019

• fix #9 (#290), improve gnosis lemmas (from PR #289)

  

  daejunpark

  authored and

  denis-bogdanas

  committed
  5743fd4

  Copy full SHA for 5743fd4

Commits on Dec 10, 2019

• uniswap/Makefile: fixing because it uses an old KEVM version (#286)

  Show description for 3a70a44
  

  denis-bogdanas

  authored and

  daejunpark

  committed
  3a70a44

  Copy full SHA for 3a70a44

• Cleanup Deposit Lemmas (#289)

  Show description for b58167c
  daejunpark

  authored
  b58167c

  Copy full SHA for b58167c

Commits on Dec 5, 2019

• Makefile: adding --z3-cnstr-timeout 100 to gnosis and deposit. (#285)

  denis-bogdanas

  authored
  6155946

  Copy full SHA for 6155946

• deposit: update kevm (#287)

  Show description for 20fdee8
  

  daejunpark

  authored and

  denis-bogdanas

  committed
  20fdee8

  Copy full SHA for 20fdee8

Commits on Dec 4, 2019

• deposit: fix semantics rule duplication (#280)

  Show description for aa9700d
  daejunpark

  authored
  aa9700d

  Copy full SHA for aa9700d

Commits on Dec 3, 2019

• Removed ` imports ETHEREUM-SIMULATION` from everywhere. Not used anyway. Required for Haskell.

  denis-bogdanas

  committed
  20e1b61

  Copy full SHA for 20e1b61

Commits on Dec 1, 2019

• erc20/gnosis: .build/kevm.rev: a version known to work - Latest commit before Vyper storage fix, new lemma

  denis-bogdanas

  committed
  bd48edb

  Copy full SHA for bd48edb

• erc20/vyper: separate KEVM version

  denis-bogdanas

  committed
  aa8ade9

  Copy full SHA for aa8ade9

• verification.k files: removed `rule #sizeWordStack ( WS , N:Int )` lemma. Doesn't seem necessary and seems to produce exponential nr of evaluation paths.

  denis-bogdanas

  committed
  0fb0022

  Copy full SHA for 0fb0022

• Fixed sum-to-n.md after KEVM update, same content as in KEVM test

  denis-bogdanas

  committed
  a84f704

  Copy full SHA for a84f704

• deposit: removed custom k/kevm - root version is same or more recent

  denis-bogdanas

  committed
  cecb5b1

  Copy full SHA for cecb5b1

• .kevm.rev: 852e14e8918eceef28d01bd1a2ab7346b4916c7e Latest master. Changes to configuration.

  denis-bogdanas

  committed
  751bb4d

  Copy full SHA for 751bb4d

• kprove.mak: separating K_VERSION_FILE location from KEVM_VERSION_FILE, to avoid having multiple unnecessary K locations.

  denis-bogdanas

  committed
  e2c2626

  Copy full SHA for e2c2626

• .k.rev: b0b7ee6c94c4efd8fbcbb17b7a068db6af184684 option --concrete-rules, same commit as for deposit

  denis-bogdanas

  committed
  76c3263

  Copy full SHA for 76c3263

• kprove.mak: support for Haskell backend, via K_BACKEND=haskell

  denis-bogdanas

  committed
  b149a05

  Copy full SHA for b149a05

Commits on Nov 30, 2019

• Verification of deposit contract (#275)

  daejunpark

  authored
  0667141

  Copy full SHA for 0667141

Commits on Nov 23, 2019

• Jenkinsfile: removing SHUTDOWN_WAIT_TIME option until K gets fixed

  denis-bogdanas

  committed
  b35dc57

  Copy full SHA for b35dc57

• kprove.mak: option to extend the command with a prefix

  denis-bogdanas

  committed
  4f85645

  Copy full SHA for 4f85645

• Jenkinsfile/ERC2--mainnet: adding --branching-allowed 16 to eliminate the need for timeout

  denis-bogdanas

  committed
  1c60647

  Copy full SHA for 1c60647

• Jenkinsfile: different heap value for kserver mode

  denis-bogdanas

  committed
  6e15bea

  Copy full SHA for 6e15bea

• Jenkinsfile: parametrize which stage to run, option to run kserver (disabled)

  Show description for d174219
  denis-bogdanas

  committed
  d174219

  Copy full SHA for d174219