Consensys / corset

4 stars 12 forks source link

Formal verification #34

Closed letypequividelespoubelles closed 7 months ago

letypequividelespoubelles commented 9 months ago

We currently have no way to ensure traces are sufficiently constrained, but we even can't know if the spec has been fully implemented in the .lisp constraints files. While debugging, it could be nice to have some checks to help finding missing constraint implementation:

delehef commented 9 months ago

we even can't know if the spec has been fully implemented in the .lisp constraints files.

That's why constraints in the spec ought to be generated from Corset LaTeX export.

letypequividelespoubelles commented 9 months ago

That's why constraints in the spec ought to be generated from Corset LaTeX export.

Ought to, but are not imho. Because we want the spec to be beautiful /readable : we add comments, and the spec constraints are sometimes adapted when written in lisp to lower number of constraint.