<div dir="auto">Good question.<div dir="auto"><br></div><div dir="auto">The reason we have bytes in there is that python has a native bytes type with syntax for bytes literals.</div><div dir="auto"><br></div><div dir="auto">However, I think it may be better to define bytes as an abbreviation of array [uint8] and forego bytes literals. I will try to port the examples to this style and see if it gets awkward for some reason </div></div><div class="gmail_extra"><br><div class="gmail_quote">On Feb 12, 2018 03:49, "Bryan Parno" <<a href="mailto:parno@cmu.edu">parno@cmu.edu</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space"><div>This seems like an excellent initiative — thanks for getting it going! </div><div><br></div><div>I’ll have to take a closer look at the examples, but I had a quick question: in the language description (<a href="https://github.com/HACS-workshop/hacspec/blob/master/LANGUAGE.md" target="_blank">https://github.com/HACS-<wbr>workshop/hacspec/blob/master/<wbr>LANGUAGE.md</a>), why is `bytes` a special type, rather than being an array of uint8? </div><br><div> <div style="color:rgb(0,0,0);font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px">Thanks,<br>-Bryan<br></div> </div> <div><br><blockquote type="cite"><div>On Feb 10, 2018, at 8:16 AM, Karthikeyan Bhargavan <<a href="mailto:karthik.bhargavan@gmail.com" target="_blank">karthik.bhargavan@gmail.com</a>> wrote:</div><br class="m_6416887479365881696Apple-interchange-newline"><div><div>Hello All,<br><br>It would be great to get some opinions on the hacspec syntax, types, and semantics.<br><br>At HACS, we started with cryptol as the initial language (which makes great sense considering the tool support.)<br>On the hackathon day, the group moved towards a subset of python, since developers/spec authors already use it as pseudocode in RFCs.<br><br>For now, we have identified a small subset of python, with static types checked with mypy.<br>We have written some specs in this subset in /specs and we believe this subset is adequate to write idiomatic specifications for most of the primitives currently in /formal-models.<br>I believe this syntax can be compiled to idiomatic Cryptol and F*, but we need to see how they translate to other formalisms.<br><br>As time goes along, we can add more constructs as needed, but let me informally describe the current features and the open questions:<br><br>INTEGERS:<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>The language includes arbitrary precision integers (int), and fixed-size integers (uint8, uint32, uint64, uint128; we can add more as needed.)<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>Standard arithmetic operators are overloaded over these integer types, and arithmetic overflows are treated with a wrapping semantics.<br>TUPLES (RECORDS?):<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>You can build and pass around tuples of values (Tuple[T1,…,Tn])<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>We have not included records yet, but we could, if desired, include JSON-like dictionaries (see the files in /test-vectors)<br>ARRAYS:<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>The only other data structures currently are arrays of fixed-length (array[T]).<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>You can read and write arrays, and you can read and write slices from arrays.<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>You can filter an array or apply a function to each element using array comprehensions (like in Python).<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>You can split an array into blocks and you can concatenate these blocks back into a flat array.<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>We are uncertain whether to include higher-order operators like map and reduce or to rely on comprehensions and for-loops instead<br>LOOPS:<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>The only looping construct is a for loop over a range.<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>If need be, we can add other looping constructs or recursion.<br>SIDE-EFFECTS (?):<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>Variables and arrays in the language can be modified, however we would like to limit all side-effects to local variables within functions.<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>Functions always return their outputs, they do not modify any of their arguments.<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>When arrays are passed into and out of functions, they are effectively copied in and copied out.<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>This part of the semantics needs some thinking and discussion to find a good middle-ground,<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>since the python syntax is naturally imperative, but most of the formal models we have looked<br><span class="m_6416887479365881696Apple-tab-span" style="white-space:pre-wrap"> </span>at find it easier to reason about purely functional specificaion.<br><br>I am sure there is much else to look at and think about, but comments on the above would already be a good start.<br><br>Best regards,<br>Karthik<br><br><br><br><br>______________________________<wbr>_________________<br>Hacspec mailing list<br><a href="mailto:Hacspec@moderncrypto.org" target="_blank">Hacspec@moderncrypto.org</a><br><a href="https://moderncrypto.org/mailman/listinfo/hacspec" target="_blank">https://moderncrypto.org/<wbr>mailman/listinfo/hacspec</a><br></div></div></blockquote></div><br></div></blockquote></div></div>