[Easycrypt-club] Some questions

Pierre-Yves Strub pierre-yves at strub.nu
Wed Mar 9 17:15:19 CET 2016

2016-03-09 16:38 GMT+01:00 Bas Spitters <b.a.w.spitters at gmail.com>:


> 1. Is it possible to execute/simulate the while-programs?

No, but this is something on our radar.

> 2. Easycrypt 0.2 still provided export to Coq by providing SMT-traces.
>    Do I understand correctly that this is now completely gone?

EasyCrypt 0.2 was not validating the SMT calls in Coq. But the hl/prhl
traces were indeed validating into CertiCrypt.

This is gone and we don't plan to have it back. EasyCrypt has its own
kernel that forms our TCB (with SMTs when used).

> 3. Why are axioms used to specify concrete functions, e.g. the reverse
> of a list ?

If I look at the List.ec theory, I see a definition for rev.

> Is there a principled reason for this, or is it just a lack of man
> power priorities?

When we started EasyCrypt, we were mostly axiomatizing datatypes,
indeed. Now, EasyCrypt embeds a HOL-like proof assistant on its own,
and we're moving away from that style. In the end, the stdlib should
be axiom free.

However, the work is not finished --- due to the lack of man power.

> 5. Coq has Locate to find stuff. This feature seems absent from easycrypt.

No, we don't have such a feature. Note that you can fill feature requests :)


> A suggestion: We are using emacs TAGS to quickly jump to definitions, etc.
> Perhaps it can be useful for easycrypt too?
> https://github.com/HoTT/HoTT/blob/master/INSTALL.md
> https://github.com/HoTT/HoTT/blob/master/Makefile.am

I'll have a look. Thanks.

-- Pierre-Yves.

More information about the Easycrypt-club mailing list