Facundo Domínguez

When fed a snapshot with empty stake, `calculatePoolDistr` produces an empty map in the specification. This is not what the implementation does. The difference is in how the specification computes...

Uniquifying kvars introduces out-of-scope names

4

`wfcUniqify` is introducing names out of scope at this point: https://github.com/ucsd-progsys/liquid-fixpoint/blob/87b09006a46cca9340e5ff2e9af28d3fa60d8509/src/Language/Fixpoint/Solver/UniqifyKVars.hs#L66 `sym` in that snippet is taken from the environment of the wf constraint of the kvar, but it is...

Implement lint checks on the input constraints

1

The README provides a few invariants that need to be checked [[link]](https://github.com/ucsd-progsys/liquid-fixpoint/blob/69194cbb99a7eebfa8e459e4e48a4dc2dbfa92e6/README.md?plain=1#L197) on the .fq queries. Perhaps some of these checks are already implemented, but that needs to be tested....

liquid-fixpoint tests fail when run from hackage

8

There are some failures when running tests from hackage. To reproduce the failures ``` nix-shell -p haskell.compiler.ghc9122 cabal-install z3 cvc5 --run "cabal unpack liquid-fixpoint" cd liquid-fixpoint-0.9.6.3.3 nix-shell -p haskell.compiler.ghc9122 cabal-install...

EverCDDL crashes on cddl specification

3

The following input causes CDDL.exe to crash, probably because it runs out of memory. The RSS grows beyond 150G at least. ``` bootstrap_witness = [ public_key : vkey , signature...