Stream: Miscellaneous

Topic: Easycrypt


view this post on Zulip Leo Colisson (Mar 07 2023 at 09:16):

Hello, I'm playing with easycrypt, but is there any reason for res < 2 to be defined (Int module) while res > 2 is not defined? It is to avoid duplicating the rules for the two versions?

view this post on Zulip Leo Colisson (Mar 07 2023 at 09:17):

Ok, I guess the fact that => already exists is also in favor of not using =>

view this post on Zulip Notification Bot (Mar 07 2023 at 09:28):

This topic was moved here from #Coq users > Easycrypt by Karl Palmskog.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2023 at 13:32):

Hi @Leo Colisson , I guess indeed EasyCrypt follows the conventions of math-comp, where x > y is just sugar for y < x, so indeed, only _ < _ is "primitive".

view this post on Zulip Bas Spitters (Mar 07 2023 at 15:34):

If you're interested in Easycrypt, then the Formosa zulip will probably give you a more detailed answer.
If you'd like to do cryptographic proofs in Coq, you could try our https://github.com/SSProve/ssprove

view this post on Zulip Leo Colisson (Mar 07 2023 at 17:21):

Thanks a lot @Bas Spitters . I was actually not aware of ssprove, I'll get it a try. @Emilio Jesús Gallego Arias Regarding x > y, as far as I tried it would not even compile as I would get a typing issue saying that > is not defined for integers, while < is (which is part of my confusion). But I guess it's just something to know about ^^ (unless I missed something)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 07 2023 at 17:35):

It's been a while since I used EC indeed, you can try the Formosa Zulip or ping @Pierre-Yves Strub who may be able to point out what the right forum is.

view this post on Zulip psilospore (Oct 22 2023 at 23:54):

Hi I'm trying to follow https://fm.csl.sri.com/SSFT23/easycrypt-tutorial.pdf but when I try stepping through proof general and get to this line:

require import CyclicGroup.

And proof general says it cannot find theory CyclicGroup. I have the file co-located and ran it with easycrypt which generates a CyclicGroup.eco object file. Not sure if there's something else I need to have setup or I'm missing something.

view this post on Zulip Bas Spitters (Oct 23 2023 at 11:44):

Again, this is a question for Formosa Zulip.

view this post on Zulip Karl Palmskog (Oct 23 2023 at 11:59):

https://formosa-crypto.zulipchat.com/ https://formosa-crypto.org/


Last updated: Jun 17 2024 at 22:01 UTC