issues
search
DavePearce
/
DevmProofGen
Dafny Evm Proof Generator (experimental)
1
stars
1
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Infinite Loop in Dependency Analysis
#104
DavePearce
opened
4 weeks ago
0
Asserts for masked addresses
#103
booleanfunction
opened
1 month ago
1
Using Sequence instead of Peek for Stack
#102
DavePearce
opened
1 month ago
2
Block Splitting on Context
#101
DavePearce
opened
2 months ago
0
Support Split At Bytecode
#100
DavePearce
opened
4 months ago
1
Write out seqs of bytecodes in chunks to work around dafny bug
#99
hmijail
closed
5 months ago
1
Partition long seqs to work around a dafny bug in v4.5+
#98
hmijail
closed
5 months ago
1
Requires `MSTORE` / `MSTORE8` address
#97
DavePearce
closed
5 months ago
0
Support for tracking mask info
#96
DavePearce
closed
5 months ago
0
Add `{:axiom}` to jump targets
#95
DavePearce
closed
5 months ago
0
Minimisation + `AND` optimisation
#94
DavePearce
closed
5 months ago
0
Minimisation and `MStore`
#93
DavePearce
closed
5 months ago
0
Symbolic Stack Information
#92
DavePearce
opened
5 months ago
1
Assumptions should use `{:axiom}`
#91
DavePearce
closed
5 months ago
0
89 support and masking
#90
DavePearce
closed
5 months ago
0
Support And Masking
#89
DavePearce
closed
5 months ago
1
Tidy up command-line options for minimisation
#88
DavePearce
closed
5 months ago
0
Tidy up Effects of Minimisation
#87
DavePearce
closed
5 months ago
0
83 minimise unnecessary intermediate values
#86
DavePearce
closed
5 months ago
0
84 bytecode should wrap instruction
#85
DavePearce
closed
6 months ago
0
`Bytecode` Should Wrap `Instruction`
#84
DavePearce
closed
6 months ago
0
Minimise Unnecessary Intermediate Values
#83
DavePearce
closed
5 months ago
3
Use `function` instead of `method`
#82
DavePearce
opened
11 months ago
0
Reinstate precondition checks
#81
DavePearce
closed
1 year ago
0
Refactor to use `State.MemSize()`
#80
DavePearce
closed
1 year ago
0
Support Intermediate Assertions
#79
DavePearce
opened
1 year ago
1
Preconditions for Zero Slot
#78
DavePearce
opened
1 year ago
2
Use `MemSize()`
#77
DavePearce
closed
1 year ago
0
Print Trace Info Prior to Next
#76
DavePearce
closed
1 year ago
0
Support `AndU8`, `AndU160`, etc
#75
DavePearce
opened
1 year ago
0
Improved Notion of Ownership
#74
DavePearce
opened
1 year ago
0
Add cli option `--devmdir`
#73
DavePearce
closed
1 year ago
0
56 block splitting algorithm
#72
DavePearce
closed
1 year ago
0
Fix for BettingContract
#71
DavePearce
closed
1 year ago
2
Add CLI option for DafnyEVM home
#70
DavePearce
closed
1 year ago
0
56 block splitting algorithm
#69
DavePearce
closed
1 year ago
0
Improved stack height preconditions
#68
DavePearce
closed
1 year ago
0
Separate "static" from "dynamic" stack items
#67
DavePearce
closed
1 year ago
0
Use set notation for `st.Operands()`
#66
DavePearce
closed
1 year ago
0
Update DafnyEvm
#65
DavePearce
closed
1 year ago
0
Support `--outdir` command-line argument
#64
DavePearce
closed
1 year ago
0
Pull out "constant" stack items
#63
DavePearce
closed
1 year ago
0
Add exclusions for invalid stack sizes
#62
DavePearce
closed
1 year ago
0
Fix translation of `call` bytecode
#61
DavePearce
closed
1 year ago
0
BitVector Operations
#60
DavePearce
opened
1 year ago
0
Support `--outdir` command line option
#59
DavePearce
closed
1 year ago
0
Fix newlines in target file
#58
DavePearce
opened
1 year ago
0
Support `staticcall`, `delegatecall`, etc.
#57
DavePearce
opened
1 year ago
0
Block Splitting Algorithm
#56
DavePearce
closed
1 year ago
3
36 group blocks
#55
DavePearce
closed
1 year ago
0
Next