<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On 10 February 2018 at 13:16, Karthikeyan Bhargavan <span dir="ltr"><<a href="mailto:karthik.bhargavan@gmail.com" target="_blank">karthik.bhargavan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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></blockquote><div><br></div><div>I was looking at those today, and I'm a bit confused - it doesn't seem possible to specify the sizes of int and bytes types?</div><div><br></div><div>Also, in the ctr.py example, is that assuming msg is some multiple of the block size?</div><div><br></div><div>We're using LIONESS at work, which is only loosely specified, and we were thinking of writing a hacspec spec for it...</div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
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>
        The language includes arbitrary precision integers (int), and fixed-size integers (uint8, uint32, uint64, uint128; we can add more as needed.)<br>
        Standard arithmetic operators are overloaded over these integer types, and arithmetic overflows are treated with a wrapping semantics.<br>
TUPLES (RECORDS?):<br>
        You can build and pass around tuples of values (Tuple[T1,…,Tn])<br>
        We have not included records yet, but we could, if desired, include JSON-like dictionaries (see the files in /test-vectors)<br>
ARRAYS:<br>
        The only other data structures currently are arrays of fixed-length (array[T]).<br>
        You can read and write arrays, and you can read and write slices from arrays.<br>
        You can filter an array or apply a function to each element using array comprehensions (like in Python).<br>
        You can split an array into blocks and you can concatenate these blocks back into a flat array.<br>
        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>
        The only looping construct is a for loop over a range.<br>
        If need be, we can add other looping constructs or recursion.<br>
SIDE-EFFECTS (?):<br>
        Variables and arrays in the language can be modified, however we would like to limit all side-effects to local variables within functions.<br>
        Functions always return their outputs, they do not modify any of their arguments.<br>
        When arrays are passed into and out of functions, they are effectively copied in and copied out.<br>
        This part of the semantics needs some thinking and discussion to find a good middle-ground,<br>
        since the python syntax is naturally imperative, but most of the formal models we have looked<br>
        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>
<br>______________________________<wbr>_________________<br>
Hacspec mailing list<br>
<a href="mailto:Hacspec@moderncrypto.org">Hacspec@moderncrypto.org</a><br>
<a href="https://moderncrypto.org/mailman/listinfo/hacspec" rel="noreferrer" target="_blank">https://moderncrypto.org/<wbr>mailman/listinfo/hacspec</a><br>
<br></blockquote></div><br></div></div>