Christian Doczkal (Jul 02 2021 at 12:56): Christian Doczkal (Jul 02 2021 at 12:56):Invited Talk given by @Vincent Laporte
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).
Enrico Tassi (Jul 02 2021 at 13:00):Here a bit of "doc": https://github.com/LPCIC/coq-elpi/tree/master/apps/derive
Christian Doczkal (Jul 02 2021 at 13:01):I was thinking precisely of that when he said that ;)
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?
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.
Vincent Laporte (Jul 02 2021 at 13:14):Thanks for the pointer, Enrico.
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)
Ben Siraphob (Jul 02 2021 at 13:19):Is there a library/framework for defining semantics for CPUs?
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
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).
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...
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)?
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.
Vincent Laporte (Jul 02 2021 at 13:51):@Ben Siraphob There is sail which looks promising.
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 boolmight 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: Apr 18 2024 at 23:01 UTC