Consensys/eth2.0-dafny

Issues

• assertion might not hold error in deserialise function

  #61 opened 9 months ago by TonyP4N
  0

• Investigate specification of `updateFinalisedCheckpoint`

  #50 opened 3 years ago by franck44
  1

• PySSZ does not allow serialising UintK values >= 2^32

  #41 opened 3 years ago by saltiniroberto
  1

• Widespread use of assert to validate method arguments

  #22 opened 3 years ago by franck44
  1

• Add process_deposit to state_transition

  #39 opened 3 years ago by franck44
  1

• Missing pre-conditions

  #34 opened 3 years ago by franck44
  1

• List types of max length 0 are legal according to the SSZ spec, but are not legal according to the pyssz reference implementation.

  #30 opened 3 years ago by saltiniroberto
  0

• Merge the two versions of fromBitlistToBytes

  #11 opened 3 years ago by franck44
  1

• on_block(b) and (store) progress

  #31 opened 3 years ago by franck44
  1

• Security vulnerabilities (possible overflows) in helper functions of Beacon Chain

  #45 opened 3 years ago by franck44
  1

• the Merkleization section of simple-serialize.md

  #33 opened 3 years ago by booleanfunction
  1

• Avoid creating "computation" overflows when not necessary

  #47 opened 3 years ago by franck44
  1

• Consistency in functions' signature and use of side-effects

  #35 opened 3 years ago by franck44
  1

• Definition of const in imported module breaks some proofs

  #25 opened 3 years ago by franck44
  1

• Warning on pre-conditions equivalent to false

  #24 opened 3 years ago by franck44
  1

• Make the specification of int_to_bytes and bytes_to_int more general

  #21 opened 3 years ago by saltiniroberto
  2

• Missing pre-condition in state_transition

  #18 opened 3 years ago by franck44
  0

• Please review commit for the xor function and related helpers

  #14 opened 3 years ago by saltiniroberto
  2

• Clarify how lists of lists are serialised

  #5 opened 3 years ago by franck44
  0

• Bug in get_next_power_of_2

  #3 opened 3 years ago by franck44
  2

• sizeOf may only be used on fixed-size objects.

  #1 opened 3 years ago by franck44
  1

• Collect stats

  #7 opened 3 years ago by franck44
  3

• Serialiased output type

  #2 opened 3 years ago by franck44
  3

• Update README

  #37 opened 3 years ago by franck44
  0

• Add entry to list of maintained SSZ implementations

  #48 opened 3 years ago by franck44
  1

• Fuel setting on a function used in a constrained type declaration erroneously affects the witness verification

  #36 opened 3 years ago by saltiniroberto
  1

• Investigate: new info Auto-accumulator tail-recursive using Dafny 3

  #49 opened 3 years ago by franck44
  3

• Definition of an inconsistent `const` can lead to unsound verification results

  #46 opened 3 years ago by franck44
  1

• Re-organise folders/files.

  #51 opened 3 years ago by franck44
  1

• Define constant for Max number of validators

  #59 opened 3 years ago by franck44
  2

• Introduce IndexedAttestation

  #60 opened 3 years ago by franck44
  1

• Simplify SSZ

  #58 opened 4 years ago by franck44
  0

• Enable per file verification configuration

  #53 opened 4 years ago by franck44
  2

• Fix proof of bitvectorEncodeDecodeIsIdentity

  #52 opened 4 years ago by franck44
  1

• Variable names clash in Boogie file

  #44 opened 4 years ago by franck44
  1

• Move to using block instead of blockHeaders

  #38 opened 4 years ago by franck44
  0

• bitfield_bytes(bits) should return chunks

  #15 opened 4 years ago by booleanfunction
  1

• to_chunks (and thus the pack function) doesn't guarantee a return of at least one chunk

  #9 opened 4 years ago by booleanfunction
  1

• SSZ spec: Merkleization - Typo in wording

  #32 opened 4 years ago by booleanfunction
  1

• Please review int_to_bytes, bytes_to_int, lemmaBytesToIntIsTheInverseOfIntToBytes, lemmaIntToBytesIsTheInverseOfBytesToInt in beacon/helpers/Math.dfy

  #19 opened 4 years ago by saltiniroberto
  3

• Make the behaviour of int_to_bytes and bytes_to_int in Math.dfy dependent on the ENDIANNESS constant

  #20 opened 4 years ago by saltiniroberto
  3

• Add Serialisation for Containers and prove related (de)serialisation lemmas.

  #26 opened 4 years ago by saltiniroberto
  0

• Deserialise bitlist accepts 0x00

  #4 opened 4 years ago by franck44
  2

• Trait code failing when using bit vector type

  #23 opened 4 years ago by franck44
  1

• An empty bitvector should be illegal in the py-ssz implementation

  #16 opened 5 years ago by booleanfunction
  2

• Conflicting definitions of BeaconBlock

  #17 opened 5 years ago by franck44
  1

• Encode Vectors only for specific cases

  #13 opened 5 years ago by franck44
  1

• Move away from using wellTyped

  #12 opened 5 years ago by franck44
  2

• Re-organise repo

  #6 opened 5 years ago by franck44
  0

• Add licensing information to repo.

  #8 opened 5 years ago by franck44
  0