pirapira/eth-isabelle issues and pull requests

#488 - Rename op to uniop because it conflicts with Isabelle's op.

Pull Request - State: open - Opened by alexaltair over 6 years ago - 1 comment

#487 - Return failure codes same as those of KEVM

Issue - State: open - Opened by pirapira over 6 years ago
Labels: enhancement

#486 - hexparser.rb should emit an error for invalid inputs

Issue - State: open - Opened by pirapira over 6 years ago
Labels: bug

#485 - Implement hash of transaction

Pull Request - State: closed - Opened by pirapira over 6 years ago

#484 - Encoding crypto parameters into RLP

Pull Request - State: closed - Opened by pirapira over 6 years ago

#483 - make lem-pdf in CircleCI

Pull Request - State: closed - Opened by pirapira over 6 years ago - 1 comment

#482 - Remove opam upgrade to fix #481

Pull Request - State: closed - Opened by pirapira over 6 years ago

#481 - Update the interface of ecdsa library, to fix OCaml build

Issue - State: closed - Opened by pirapira over 6 years ago

#480 - Show termination of sha3_update

Pull Request - State: closed - Opened by pirapira over 6 years ago - 1 comment

#479 - Add Byzantium instructions

Issue - State: open - Opened by pirapira over 6 years ago
Labels: enhancement

#478 - Generate sha3_update not as a function but as a fun

Issue - State: closed - Opened by pirapira over 6 years ago - 1 comment
Labels: bug

#477 - Encode transaction_to into RLP

Pull Request - State: closed - Opened by pirapira almost 7 years ago - 1 comment

#476 - GlobalTriple theory should be checked in the continuous integration systems

Issue - State: open - Opened by pirapira almost 7 years ago

#475 - Encode the value of a transaction into RLP

Pull Request - State: closed - Opened by pirapira almost 7 years ago

#474 - Gas price as RLP

Pull Request - State: closed - Opened by pirapira almost 7 years ago

#473 - Add a dependency information in README

Pull Request - State: closed - Opened by pirapira almost 7 years ago

#472 - Execute blockchain test---partial progress with build changes

Pull Request - State: closed - Opened by pirapira almost 7 years ago

#471 - Add Vault.thy

Pull Request - State: closed - Opened by pirapira almost 7 years ago

#470 - Rename rlp.lem into rlplem.lem to avoid name collision with Rlp.ml ex…

Pull Request - State: closed - Opened by pirapira almost 7 years ago
Labels: in progress

#469 - Fix an error in lem-pdf

Pull Request - State: closed - Opened by pirapira almost 7 years ago

#468 - Change the behavior of `make` because ROOT does not contain the sessi…

Pull Request - State: closed - Opened by pirapira almost 7 years ago

#467 - Fix the build of EvmFacts.thy

Issue - State: open - Opened by pirapira almost 7 years ago

#466 - Fix the build of GlobalTriple.thy

Issue - State: open - Opened by pirapira almost 7 years ago

#465 - Trying to fix the Continuous Integration builds

Pull Request - State: closed - Opened by pirapira almost 7 years ago

#464 - Spurious failures in Travis

Issue - State: open - Opened by pirapira almost 7 years ago

#463 - vmtest calldataload1 yields "Some post conditions not available"

Issue - State: open - Opened by pirapira almost 7 years ago - 3 comments

#462 - Basic block program logic

Pull Request - State: closed - Opened by seed almost 7 years ago - 5 comments

#461 - Fix Isabelle versions in README

Pull Request - State: closed - Opened by pirapira about 7 years ago

#460 - Hoare logic with invariants, beginning steps

Pull Request - State: closed - Opened by pirapira about 7 years ago

#459 - Apply Byzantium changes

Issue - State: open - Opened by pirapira about 7 years ago

#458 - Fix the script GlobalTriple

Issue - State: open - Opened by pirapira about 7 years ago
Labels: bug, accepted

#457 - Fix the script EvmFacts.thy

Issue - State: open - Opened by pirapira about 7 years ago
Labels: bug, accepted

#456 - Rename 'next' in block.lem into 'step'

Pull Request - State: closed - Opened by pirapira about 7 years ago

#455 - Isabelle2017

Pull Request - State: closed - Opened by pirapira about 7 years ago

#454 - An ML type error in Apply_Trace.thy with Isabelle2017

Issue - State: open - Opened by pirapira about 7 years ago - 1 comment

#453 - Isabelle 2017

Issue - State: closed - Opened by pirapira about 7 years ago - 1 comment

#452 - Add an address-to-byte-list conversion

Pull Request - State: closed - Opened by pirapira about 7 years ago

#451 - Remove some warnings during make lem-ocaml

Pull Request - State: closed - Opened by pirapira about 7 years ago

#450 - This commit fixes Holmake evmTheory.uo

Pull Request - State: closed - Opened by pirapira about 7 years ago

#449 - HOL4 Can't Prove Termination of log2

Issue - State: closed - Opened by mmalvarez about 7 years ago - 3 comments
Labels: bug

#448 - Exclude program_sem_t from Coq extraction

Pull Request - State: closed - Opened by pirapira about 7 years ago

#447 - Compare the behavior the Julia compiler and Julia specification

Issue - State: open - Opened by pirapira over 7 years ago
Labels: enhancement

#446 - Julia (Solidity IR) specification / interpreter

Pull Request - State: closed - Opened by mrsmkl over 7 years ago - 2 comments

#445 - make lem-pdf fails

Issue - State: open - Opened by pirapira over 7 years ago
Labels: bug, soon

#444 - Alternative version of program_sem that terminates using gas consumption arguement.

Pull Request - State: closed - Opened by seed over 7 years ago - 3 comments
Labels: needs review

#443 - Fixed HoareTripleForMemory.thy, MLOAD, MSTORE, but not SHA3

Pull Request - State: closed - Opened by mrsmkl over 7 years ago - 1 comment

#442 - Termination, Balance proofs, theory for re-entrance

Pull Request - State: closed - Opened by mrsmkl over 7 years ago - 2 comments

#441 - Rename `no_annotation_failure` into `invariant_holds` because the ann…

Pull Request - State: closed - Opened by pirapira over 7 years ago

#440 - Fix SimpleWallet and add it to the Travis build

Pull Request - State: closed - Opened by pirapira over 7 years ago

#439 - Fix check in Cgascap to account for memu_extra.

Pull Request - State: closed - Opened by seed over 7 years ago - 1 comment

#438 - Pirapira master

Pull Request - State: closed - Opened by seed over 7 years ago - 1 comment

#437 - Implement EIP 170: max code size

Issue - State: open - Opened by pirapira over 7 years ago
Labels: bug, accepted

#436 - Undefined bundle: "sep_crunch"

Issue - State: closed - Opened by pirapira over 7 years ago - 4 comments
Labels: bug

#435 - Add a missing dependency to all-isabelle

Pull Request - State: closed - Opened by pirapira over 7 years ago

#434 - Add Coq build to circle CI

Pull Request - State: closed - Opened by pirapira over 7 years ago

#433 - Add CircleCI badge

Pull Request - State: closed - Opened by pirapira over 7 years ago

#432 - Add Circle CI setting

Pull Request - State: closed - Opened by pirapira over 7 years ago

#431 - "invalid digit" failure during vmtest

Issue - State: closed - Opened by pirapira over 7 years ago - 2 comments
Labels: bug, next release

#430 - add a coq build to circleCI

Issue - State: closed - Opened by pirapira over 7 years ago

#429 - Fix Coq compilation

Pull Request - State: closed - Opened by pirapira over 7 years ago

#428 - Set up the cache configuration for CircleCI

Issue - State: closed - Opened by pirapira over 7 years ago

#427 - Add a link to the EVM formalizaiton in K framework

Pull Request - State: closed - Opened by pirapira over 7 years ago

#426 - Snatching @seed's pirapira-master branch

Pull Request - State: closed - Opened by pirapira over 7 years ago

#425 - Try Wercker for continuous integration

Issue - State: open - Opened by pirapira over 7 years ago
Labels: soon

#424 - Try Circle CI

Issue - State: closed - Opened by pirapira over 7 years ago

#423 - Remove Deed.thy because it is not maintained

Pull Request - State: closed - Opened by pirapira over 7 years ago - 2 comments

#422 - Figure out the sender of a transaction

Issue - State: open - Opened by pirapira over 7 years ago
Labels: in progress

#421 - Gas price belongs to the transaction not the block

Pull Request - State: closed - Opened by pirapira over 7 years ago - 1 comment

#420 - Compile error: Stackoverflow or Segmentation fault

Issue - State: closed - Opened by renovatorruler over 7 years ago - 3 comments
Labels: bug

#419 - Remove annotations

Pull Request - State: closed - Opened by pirapira over 7 years ago - 1 comment

#418 - fix warninigs from ocaml compilation

Issue - State: open - Opened by pirapira over 7 years ago
Labels: soon, next release

#417 - fix warnings from lem-ocaml

Issue - State: closed - Opened by pirapira over 7 years ago - 1 comment

#416 - fix warnings from lem-ocaml

Issue - State: open - Opened by pirapira over 7 years ago
Labels: soon, next release

#415 - TraverseJsons: skip non .json files

Pull Request - State: closed - Opened by pirapira over 7 years ago - 1 comment

#414 - Use a new version of ethereum/tests

Pull Request - State: closed - Opened by pirapira over 7 years ago

#413 - Fix AlwaysFail and add it to the Travis CI build

Pull Request - State: closed - Opened by pirapira over 7 years ago

#412 - `next` is a keyword in Isabelle, so avoid the name in block.lem

Issue - State: closed - Opened by pirapira over 7 years ago
Labels: next release

#411 - Fix sstore_gas_triple lemma

Pull Request - State: closed - Opened by pirapira over 7 years ago

#410 - Test the EVM using Coq to OCaml extraction

Issue - State: open - Opened by pirapira over 7 years ago
Labels: accepted

#409 - Traverse directories for json files

Pull Request - State: closed - Opened by pirapira over 7 years ago

#408 - Fix SimpleWallet.thy

Issue - State: closed - Opened by pirapira over 7 years ago - 1 comment

#407 - Fix call gas triple

Pull Request - State: closed - Opened by pirapira over 7 years ago

#406 - Add AccountExistent predicate element

Pull Request - State: closed - Opened by pirapira over 7 years ago

#405 - Parse blockchain test

Pull Request - State: closed - Opened by pirapira over 7 years ago

#404 - Use externally specified protocol version

Pull Request - State: closed - Opened by pirapira over 7 years ago

#403 - Remove aenv and annotation from the definitions

Issue - State: closed - Opened by pirapira over 7 years ago
Labels: next release

#402 - Move Parse.thy out of attic and test it in Travis

Pull Request - State: closed - Opened by pirapira over 7 years ago

#401 - Parser and inst_stack_nb

Pull Request - State: closed - Opened by mbegel over 7 years ago - 2 comments

#392 - Skip state tests that cause out of memory in OCaml runtime

Issue - State: open - Opened by pirapira over 7 years ago - 1 comment
Labels: next release

#361 - Add a script to run all state tests

Issue - State: open - Opened by pirapira over 7 years ago
Labels: soon

#349 - Fix proofs in example/termination

Issue - State: open - Opened by pirapira over 7 years ago
Labels: bug, accepted

#345 - Mstore8 mem usage

Pull Request - State: closed - Opened by seed over 7 years ago

#341 - Formalize the Metropolis changes

Issue - State: open - Opened by pirapira over 7 years ago
Labels: accepted, next release

#331 - Model the environment's moves in the Hoare logic setup

Issue - State: open - Opened by pirapira over 7 years ago
Labels: accepted

#289 - Streamline the proof of STOP triple

Issue - State: open - Opened by pirapira almost 8 years ago
Labels: soon

#249 - Reduce output from runVmTest.native

Issue - State: open - Opened by pirapira almost 8 years ago
Labels: soon

#242 - specify RETURN as a Hoare triple

Issue - State: open - Opened by pirapira almost 8 years ago - 1 comment
Labels: accepted

#241 - specify CALLCODE as a Hoare triple

Issue - State: open - Opened by pirapira almost 8 years ago
Labels: accepted

#129 - Add missing quantifiers in evmNonExec.lem

Issue - State: open - Opened by pirapira almost 8 years ago
Labels: bug, accepted

#120 - Prove a Hoare Triple for CALLDATALOAD

Issue - State: open - Opened by pirapira almost 8 years ago
Labels: accepted

GitHub / pirapira/eth-isabelle issues and pull requests