pirapira/eth-isabelle

Issues

• Return failure codes same as those of KEVM

  #487 opened 7 years ago by pirapira
  0

• hexparser.rb should emit an error for invalid inputs

  #486 opened 7 years ago by pirapira
  0

• Generate sha3_update not as a function but as a fun

  #478 opened 7 years ago by pirapira
  1

• Update the interface of ecdsa library, to fix OCaml build

  #481 opened 7 years ago by pirapira
  0

• Add Byzantium instructions

  #479 opened 7 years ago by pirapira
  0

• GlobalTriple theory should be checked in the continuous integration systems

  #476 opened 7 years ago by pirapira
  0

• Fix the build of EvmFacts.thy

  #467 opened 7 years ago by pirapira
  0

• Fix the build of GlobalTriple.thy

  #466 opened 7 years ago by pirapira
  0

• Spurious failures in Travis

  #464 opened 7 years ago by pirapira
  0

• vmtest calldataload1 yields "Some post conditions not available"

  #463 opened 7 years ago by pirapira
  3

• make lem-pdf fails

  #445 opened 7 years ago by pirapira
  0

• "invalid digit" failure during vmtest

  #431 opened 7 years ago by pirapira
  2

• Apply Byzantium changes

  #459 opened 7 years ago by pirapira
  0

• Fix the script EvmFacts.thy

  #457 opened 7 years ago by pirapira
  0

• Fix the script GlobalTriple

  #458 opened 7 years ago by pirapira
  0

• `next` is a keyword in Isabelle, so avoid the name in block.lem

  #412 opened 7 years ago by pirapira
  0

• Isabelle 2017

  #453 opened 7 years ago by pirapira
  1

• An ML type error in Apply_Trace.thy with Isabelle2017

  #454 opened 7 years ago by pirapira
  1

• Compare the behavior the Julia compiler and Julia specification

  #447 opened 7 years ago by pirapira
  0

• HOL4 Can't Prove Termination of log2

  #449 opened 7 years ago by mmalvarez
  3

• Fix SimpleWallet.thy

  #408 opened 7 years ago by pirapira
  1

• Remove aenv and annotation from the definitions

  #403 opened 7 years ago by pirapira
  0

• fix warnings from lem-ocaml

  #416 opened 8 years ago by pirapira
  0

• fix warninigs from ocaml compilation

  #418 opened 8 years ago by pirapira
  0

• Skip state tests that cause out of memory in OCaml runtime

  #392 opened 8 years ago by pirapira
  1

• Undefined bundle: "sep_crunch"

  #436 opened 7 years ago by pirapira
  4

• Implement EIP 170: max code size

  #437 opened 7 years ago by pirapira
  0

• add a coq build to circleCI

  #430 opened 7 years ago by pirapira
  0

• Compile error: Stackoverflow or Segmentation fault

  #420 opened 7 years ago by renovatorruler
  3

• Try Circle CI

  #424 opened 7 years ago by pirapira
  0

• Set up the cache configuration for CircleCI

  #428 opened 7 years ago by pirapira
  0

• Test the EVM using Coq to OCaml extraction

  #410 opened 8 years ago by pirapira
  0

• Try Wercker for continuous integration

  #425 opened 7 years ago by pirapira
  0

• Figure out the sender of a transaction

  #422 opened 7 years ago by pirapira
  0

• fix warnings from lem-ocaml

  #417 opened 8 years ago by pirapira
  1

• Parse and execute BlockChainTests

  #400 opened 8 years ago by pirapira
  0

• Detect precompile invocations in state tests

  #372 opened 8 years ago by pirapira
  1

• stateTest.ml should report the number of skipped / failed / successful tests

  #386 opened 8 years ago by pirapira
  1

• Five-wei balance difference in a state test

  #397 opened 8 years ago by pirapira
  3

• Different storage in CreateAndGasInsideCreate test

  #395 opened 8 years ago by pirapira
  3

• Different nonce value in `recursiveCreateReturnValue`.

  #393 opened 8 years ago by pirapira
  2

• Solve stackoverflow during state tests

  #371 opened 8 years ago by pirapira
  0

• Calling precompiled contracts should cause "Unimplemented" result

  #378 opened 8 years ago by pirapira
  0

• make sure failed_for_reasons {} x to be False

  #382 opened 8 years ago by pirapira
  1

• A script that creates a tar ball containing Coq files

  #379 opened 8 years ago by pirapira
  0

• Implement the precompiled contract for identity

  #377 opened 8 years ago by pirapira
  0

• Travis script should create tar balls containing Coq sources on github.io pages

  #380 opened 8 years ago by pirapira
  0

• Implement precompiled contract for RIPEMD160

  #376 opened 8 years ago by pirapira
  0

• Implement precompiled contract for SHA2-256

  #375 opened 8 years ago by pirapira
  0

• Implement precompiled contract for ecrecover

  #374 opened 8 years ago by pirapira
  0