NethermindEth/horus-checker

Issues

• `horus-compile` raises a `typeguard` runtime error on Python 3.9

  #197 opened 2 years ago by langfield
  1

• The semantics of operator `/` in assertions is not the proper `felt` semantics

  #161 opened 2 years ago by aemartinez
  2

• Something is wrong with the implications in queries

  #170 opened 2 years ago by langfield
  2

• How to use loop invariants

  #177 opened 2 years ago by Leonard-Pat
  7

• Checking storage update of external contract

  #173 opened 2 years ago by Leonard-Pat
  3

• Are `@storage_update` annotations supported in namespaces?

  #174 opened 2 years ago by Leonard-Pat
  1

• Possibility to see the counter-example generated by the SMT solver

  #169 opened 2 years ago by acmLL
  10

• Strange syntax error from `horus-compile` for non-imported function in separate module

  #163 opened 2 years ago by langfield
  1

• Contradictory premises

  #167 opened 2 years ago by acmLL
  2

• Namespaces cause unpredictable change in behaviour

  #151 opened 2 years ago by Ferinko
  2

• Revertable function

  #150 opened 2 years ago by acmLL
  7

• Example usage from `README.md` is missing `spec.json` argument to `horus-check`

  #157 opened 2 years ago by langfield
  0

• Installing with docker yields error: `cannot open scripts/ci/install-mathsat-linux.sh: No such file`

  #148 opened 2 years ago by acmLL
  3

• Improper interaction of @invariant/@assert with manipulation of builtin pointers.

  #125 opened 2 years ago by Ferinko
  0

• Docs - random thoughts

  #81 opened 2 years ago by Ferinko
  2