pirapira/eth-isabelle issues and pull requests

#100 - Verification condition generation

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

#99 - Design the interface to specify the target EVM version

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

#98 - Coq extraction of evm.lem in Makefile

Issue - State: closed - Opened by pirapira almost 8 years ago - 1 comment

#97 - Create make test goal

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

#96 - Copy valid contents from Lem-produced auxiliary files

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

#95 - Execute VM tests that involve multiple contracts

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

#94 - Keep track of the events logged during the execution

Issue - State: closed - Opened by pirapira almost 8 years ago - 1 comment

#93 - Build a simple vault using the simple Hoare logic

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

#92 - Specify simple instructions using Hoare triples

Issue - State: closed - Opened by pirapira almost 8 years ago - 1 comment

#91 - While lemma for Hoare triple validities

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

#90 - If-then-else lemma for Hoare triple validity

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

#89 - Sequenting lemma for Hoare triple validities

Issue - State: closed - Opened by pirapira almost 8 years ago - 1 comment

#88 - Validity relation for Hoare triples, with calling out other accounts

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

#87 - Validity relation for Hoare triples, without calling out other accounts

Issue - State: closed - Opened by pirapira almost 8 years ago

#86 - Release 0.0.1

Issue - State: closed - Opened by pirapira almost 8 years ago - 2 comments

#85 - Plan a milestone for simple hoare logic

Issue - State: closed - Opened by pirapira almost 8 years ago - 1 comment

#84 - bytecode printer

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

#83 - Remove invalid SWAP and DUP instructions

Issue - State: closed - Opened by pirapira almost 8 years ago
Labels: breaking

#82 - Remove Lem Warnings

Issue - State: closed - Opened by pirapira almost 8 years ago - 1 comment

#81 - The Isabelle extraction of `sha3_update` should use `primrec` not `function` keyword

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

#80 - Instead of listing VMtest json files, introduce a loop

Issue - State: closed - Opened by pirapira almost 8 years ago - 1 comment
Labels: enhancement

#79 - Implement the fake block hash for VM test

Issue - State: closed - Opened by pirapira almost 8 years ago

#78 - Revert 150.1b before the block 2463000

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

#77 - Isabelle 2016-1

Issue - State: closed - Opened by pirapira almost 8 years ago

#76 - Fix the parser in Parser.thy

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

#75 - Split the instruction_sem function into several smaller ones, following the definition of instructions

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

#74 - Decide the form of properties about program snippets.

Issue - State: closed - Opened by pirapira almost 8 years ago - 1 comment

#73 - only pass relevant fields to instruction_failure_result

Issue - State: closed - Opened by pirapira almost 8 years ago - 1 comment

#72 - relocatable program snippet representation

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

#71 - verify and deploy the author's wallet

Issue - State: closed - Opened by pirapira almost 8 years ago

#70 - define procedures and procedure calls and create lemmata for pre- and post- conditions

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

#69 - define while as a higher order function and prove lemmata about pre and post-conditions.

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

#68 - define ifthenelse as a higher-order function and prove lemmata around pre-post conditions

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

#67 - develop compositional reasoning method on a multisig wallet

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

#66 - only expand binary appending when program counter is wanted

Issue - State: closed - Opened by pirapira almost 8 years ago - 1 comment

#65 - port KEC.thy into Lem

Issue - State: closed - Opened by pirapira almost 8 years ago - 1 comment

#64 - replace `nat` in Lem files with `int`

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

#63 - Accept zero as a valid jump destination

Issue - State: closed - Opened by pirapira about 8 years ago - 1 comment
Labels: bug

#62 - get LaTeX document from Lem files, as a readable document

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

#61 - copy comments into the Lem files

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

#60 - add Lem files to the repository

Issue - State: closed - Opened by pirapira about 8 years ago

#59 - implement logs

Issue - State: closed - Opened by pirapira about 8 years ago

#58 - refactor the lem code to abstract away the program lookup mechanism

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

#57 - refactor the isabelle hol code to abstract away the program lookup mechanism

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

#56 - Test the EVM definition against the main net log

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

#55 - Try the ocaml extraction of ethereum-lem

Issue - State: closed - Opened by pirapira about 8 years ago

#54 - find out if lem to isabelle/hol translation keeps comments

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

#53 - Check the gas inefficiency

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

#52 - Add invariants to DELEGATECALL and CALLCODE instructions

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

#51 - Find out how to define inductive relation in Lem

Issue - State: closed - Opened by pirapira about 8 years ago

#50 - Interface for importing invariants for DELEGATECALL

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

#49 - Turning the definitions into Lem

Issue - State: closed - Opened by pirapira about 8 years ago

#48 - Update the memory in build_venv_returned

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

#47 - Prove that a non-registrar cannot change the registrar

Issue - State: closed - Opened by pirapira about 8 years ago

#46 - Try to verify a very simple program with loops

Issue - State: open - Opened by pirapira about 8 years ago
Labels: ready, accepted

#45 - compare optimized bytecode and the original

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

#44 - Consider making return_result richer

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

#43 - Model the stack limitation

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

#42 - Model callstack-depth limitations, perhaps

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

#41 - Verify simple optimization rules in ExpressionClasses.cpp

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

#40 - Prove that only registrar can destroy the Deed contract

Issue - State: closed - Opened by pirapira about 8 years ago

#39 - Beautiful PDF for Deed.thy

Issue - State: closed - Opened by pirapira about 8 years ago

#38 - Beautiful PDF for Instructions.thy

Issue - State: closed - Opened by pirapira about 8 years ago
Labels: ready

#37 - BeautifulPDF for ContractEnv.thy

Issue - State: closed - Opened by pirapira about 8 years ago

#36 - Beautiful PDF for RelationalSem.thy

Issue - State: closed - Opened by pirapira about 8 years ago

#35 - Beautiful PDF for ContractSem.thy

Issue - State: closed - Opened by pirapira about 8 years ago

#34 - The effect of suicide should not be visible to the caller

Issue - State: closed - Opened by pirapira about 8 years ago

#33 - Fix the proof in Deed.thy

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

#32 - Calling the extracted EVM implementation in OCaml on the EVM tests

Issue - State: closed - Opened by pirapira about 8 years ago
Labels: ready

#31 - Parsing VMTests in OCaml

Issue - State: closed - Opened by pirapira about 8 years ago - 1 comment
Labels: ready

#30 - Exctract the EVM implementation into OCaml

Issue - State: closed - Opened by pirapira about 8 years ago
Labels: ready

#29 - Fix the semantics of `selfdestruct`

Issue - State: closed - Opened by pirapira about 8 years ago
Labels: bug

#28 - Change the ruby parser so that it returns a binary tree, not a list

Issue - State: open - Opened by pirapira about 8 years ago
Labels: ready

#27 - Store annotations in an AVL tree

Issue - State: closed - Opened by pirapira about 8 years ago - 1 comment
Labels: ready

#26 - Store instructions in an AVL tree

Issue - State: closed - Opened by pirapira about 8 years ago - 4 comments

#25 - Decompose variable_env record in the performance critical paths

Issue - State: open - Opened by pirapira about 8 years ago
Labels: ready

#24 - Streamline the definition of `jump`

Issue - State: open - Opened by pirapira about 8 years ago
Labels: ready

#23 - Try the new debugger for Isabelle simplification

Issue - State: closed - Opened by pirapira about 8 years ago - 2 comments

#22 - venv_advance_pc should not take the constant environment as an argument but a number

Issue - State: open - Opened by pirapira about 8 years ago
Labels: ready

#21 - Only expand the definition of the program when a concrete program counter is known

Issue - State: open - Opened by pirapira about 8 years ago
Labels: ready

#20 - Optimize the speed of simplification

Issue - State: closed - Opened by pirapira about 8 years ago - 3 comments

#19 - Optimize the size of the proof goals

Issue - State: closed - Opened by pirapira about 8 years ago - 2 comments

#18 - Performance issue around 500 bytes of program

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

#17 - Verify a pair of a precondition and a postcondition for a whole invocation

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

#16 - Verify programs with loops

Issue - State: open - Opened by pirapira about 8 years ago - 4 comments
Labels: enhancement, accepted

#15 - A Makefile that checks compilation of all files

Issue - State: closed - Opened by pirapira about 8 years ago - 1 comment
Labels: ready

#14 - Disallow returning to a location not after CALL, DELEGATECALL, CALLCODE or CREATE

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

#13 - Change the typename uint into word256

Issue - State: closed - Opened by pirapira about 8 years ago - 2 comments

#12 - Try encoding a program as (pc => instruction) to see if it's more efficient

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

#11 - Verify the Deed contract

Issue - State: closed - Opened by pirapira about 8 years ago - 6 comments

#10 - Remove `let` from the definitions

Issue - State: open - Opened by pirapira about 8 years ago
Labels: ready

#9 - Try relational semantics

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

#8 - Prove a theorem that the memory is all zero above memory_usage

Issue - State: open - Opened by pirapira about 8 years ago
Labels: ready

#7 - Implement gas

Issue - State: closed - Opened by pirapira about 8 years ago - 1 comment
Labels: ready

#6 - Implement a predicate that judges if all assertions hold after any history

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

#5 - Test the EVM in Isabelle/HOL against the usual EVM tests

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

#4 - Support verification of bytecode fragments

Issue - State: open - Opened by pirapira about 8 years ago
Labels: ready

#3 - Check if (min-sint / (-1)) is implemented in the same way as in the EVM

Issue - State: closed - Opened by pirapira about 8 years ago

#2 - Support all opcodes

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

#1 - Allow annotations before JUMPDEST

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

GitHub / pirapira/eth-isabelle issues and pull requests