Shumo Chu

@zedware which result did you get? I assume it is `UNKNOWN`?

@zedware thank you! this is a known issue. currently we don't interpret predicate. We are working on Cosette 2.0 that will fix this issue.

Interesting! Thanks for the issue.

Thanks for the bug report! There is a minor mistake in Coq code generation. @duremar I believe this is fixed through `43cbd27`. The web frontend deployment takes about 15 mins...

I will put this as a post 2.0 issue.

Thanks for the report. This looks like an edge case in prover code gen.

Thanks! @Njanderson That's one of the known problems. We will fix this in the next version. Unfortunately, it will take some time. One thing that may help is, I would...

@vinvsv97 we hear you. This is a known issue. Unfortunately, I don't have any cycle right now. Will fix it after May 15th.

@fuyfuy Thanks for your suggestion. I think we can include CTE in the next version of Cosette.

Does `PseudoRandomFunction ` imply `CollisionResistantHashing`?