Zoe Paraskevopoulou
Zoe Paraskevopoulou
It would be very useful to add support for primitive ints + floats in MetaCoq (so we can then realize such primitives in CertiCoq's backend). Are there any plans to...
Apply the new size-free methodology to the STLC case study.
Features and bug fixes: - Adds support for environment values in the Coq backend (only CALLER atm) - Adds support for multiple updates to state variables - Bug fix in...
This PR adds assertions that storage variables that are not explicitly modified remain constant. This was missing from the SMT encoding of postconditions. Also, adds the AMΜ contract as a...
In the `amm-test` branch, trying to build the Act executable with ``` > nix develop > make ``` Fails with the error included below. Note that this is not happening...
## Proper handling of initial state so that it is not threaded Previously the state was treaded between rewrites, which is not the correct semantics of Act. Now the left...
Do not `cd src` to run cabal tests, since act.cabal is in the top-level directory.
We need to have a more principled approach to generate arithmetic bounds for storage variables. Right now: - `inRange` assertions in preconditions might generate duplicate bounds assertions as Enrich already...
It can be nice to have a `public` keyword for storage variables in Act so we can generate getter specs automatically.
- Pass fresh address counter to `makeVM` to avoid creating non-fresh addresses. - Add constraints about fresh addresses created by behaviours. - Add new tests where new contracts are created...