Stream: Coq Workshop 2021

Topic: [IT] Jasmin: Certified Workbench ...


view this post on Zulip Christian Doczkal (Jul 02 2021 at 12:56):

Invited Talk given by @Vincent Laporte

view this post on Zulip Enrico Tassi (Jul 02 2021 at 12:59):

About rose trees, you may give a look at Coq-Elpi's derive facility, see also https://drops.dagstuhl.de/opus/volltexte/2019/11084/pdf/LIPIcs-ITP-2019-29.pdf (the running example is rose trees).

view this post on Zulip Enrico Tassi (Jul 02 2021 at 13:00):

Here a bit of "doc": https://github.com/LPCIC/coq-elpi/tree/master/apps/derive

view this post on Zulip Christian Doczkal (Jul 02 2021 at 13:01):

I was thinking precisely of that when he said that ;)

view this post on Zulip Bas Spitters (Jul 02 2021 at 13:01):

Thanks for the nice talk!
Non-urgent remark/question: We've used the compcert library for machine integers in hacspec. Would it be suitable for jasmin too?

view this post on Zulip Vincent Laporte (Jul 02 2021 at 13:12):

IIRC, the issue with that library is that there are little or no mixed-size operations. These are very useful for specifying vector operations. There are also some funny instructions (e.g., RCL) that operate on bitvectors of size (2^n)+1.

view this post on Zulip Vincent Laporte (Jul 02 2021 at 13:14):

Thanks for the pointer, Enrico.

view this post on Zulip Reynald Affeldt (Jul 02 2021 at 13:19):

A long time ago we wrote a library of machine integers that were just list of bits with the size appearing in the type (it was in 2006, today it would be n.-tuple bool), we found this type nice to mix machine integers of various sizes (archive: https://github.com/affeldt-aist/seplog/blob/master/lib/machine_int.v)

view this post on Zulip Ben Siraphob (Jul 02 2021 at 13:19):

Is there a library/framework for defining semantics for CPUs?

view this post on Zulip Bas Spitters (Jul 02 2021 at 13:27):

It would be nice to have some sort of standardized machine integers for Coq
https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/unsigned.20integer.20library.20using.20Cyclic.3F

view this post on Zulip Vincent Laporte (Jul 02 2021 at 13:29):

Reynald, an other requirement for our ideal library, is that the semantics of Jasmin programs is executable: there is a reference interpreter that just runs the semantics (after extraction to OCaml). I fear that 256.-tuple bool might show bad performances on non-trivial examples (but I’d love to be proved wrong).

view this post on Zulip Christian Doczkal (Jul 02 2021 at 13:30):

IIRC, Tuple is a dependent pair of a list and proof of its length. So yes, you don't have random access...

view this post on Zulip Christian Doczkal (Jul 02 2021 at 13:36):

@Vincent Laporte In your talk you said that (argument) variables "x" and "y" are always different. Does that mean it is illegal to call a jasmin function h as h(a,a)?

view this post on Zulip Vincent Laporte (Jul 02 2021 at 13:38):

It is not illegal. It has a well-defined semantics (this is not UB, as they say in C parlance). You can use this program, e.g. within a proof or run it through the interpreter. However, the compiler will fail at compiling this program.

view this post on Zulip Vincent Laporte (Jul 02 2021 at 13:51):

@Ben Siraphob There is sail which looks promising.

view this post on Zulip Reynald Affeldt (Jul 02 2021 at 14:04):

Vincent Laporte said:

Reynald, an other requirement for our ideal library, is that the semantics of Jasmin programs is executable: there is a reference interpreter that just runs the semantics (after extraction to OCaml). I fear that 256.-tuple bool might show bad performances on non-trivial examples (but I’d love to be proved wrong).

Yes, indeed, that won't fly as such ^_^. In the end, execution of bitstrings eventually led us to custom OCaml extraction (https://staff.aist.go.jp/tanaka-akira/succinct/succinct-icfem2016-author.pdf) or C extraction (https://www.jstage.jst.go.jp/article/ipsjjip/26/0/26_54/_pdf/-char/en) (to have random access).


Last updated: Aug 11 2022 at 02:03 UTC