[hacspec] hacspec syntax

[Karthikeyan Bhargavan]

> 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?

This is a good point and shows up the limitations of the current python-based type system.
Since we are working in a subset of python and are typechecking our code via mypy,
we cannot currently state or check sizes of types.

This brings up a question: should we introduce general refinement types?
E.g. poly1305_field = x:int{x >= 0 && x < 2**130 - 5}

Or at the very least, should we add length annotations a la rust?
E.g. chacha20_state = array[uint32; 16]

If we want to stay within Python, we would ned to hide such annotations within comments.
The benefit of sticking within Python syntax is that the code is immediately executable without any preprocessing.
However, if the syntax starts getting awkward, we should be open to adding a “light” erasure step that throws away some annotations.

> Also, in the ctr.py example, is that assuming msg is some multiple of the block size?

In counter_mode(), msg has an arbitrary size.
In block_encrypt() msg has size <= blocksize.

If msg < blocksize, then zip(keyblock,msg) truncates the result to the shorter length.
I realize this is confusing and undocumented, and I’ll try to rewrite this.


> We're using LIONESS at work, which is only loosely specified, and we were thinking of writing a hacspec spec for it…

That would be great. I am trying to get my students to write specs for Curve25519, SHA-2, AES, etc. but getting a diverse set of specs will shake out the syntax.

-Karthik

> 
> 
> I believe this syntax can be compiled to idiomatic Cryptol and F*, but we need to see how they translate to other formalisms.
> 
> As time goes along, we can add more constructs as needed, but let me informally describe the current features and the open questions:
> 
> INTEGERS:
>         The language includes arbitrary precision integers (int), and fixed-size integers (uint8, uint32, uint64, uint128; we can add more as needed.)
>         Standard arithmetic operators are overloaded over these integer types, and arithmetic overflows are treated with a wrapping semantics.
> TUPLES (RECORDS?):
>         You can build and pass around tuples of values (Tuple[T1,…,Tn])
>         We have not included records yet, but we could, if desired, include JSON-like dictionaries (see the files in /test-vectors)
> ARRAYS:
>         The only other data structures currently are arrays of fixed-length (array[T]).
>         You can read and write arrays, and you can read and write slices from arrays.
>         You can filter an array or apply a function to each element using array comprehensions (like in Python).
>         You can split an array into blocks and you can concatenate these blocks back into a flat array.
>         We are uncertain whether to include higher-order operators like map and reduce or to rely on comprehensions and for-loops instead
> LOOPS:
>         The only looping construct is a for loop over a range.
>         If need be, we can add other looping constructs or recursion.
> SIDE-EFFECTS (?):
>         Variables and arrays in the language can be modified, however we would like to limit all side-effects to local variables within functions.
>         Functions always return their outputs, they do not modify any of their arguments.
>         When arrays are passed into and out of functions, they are effectively copied in and copied out.
>         This part of the semantics needs some thinking and discussion to find a good middle-ground,
>         since the python syntax is naturally imperative, but most of the formal models we have looked
>         at find it easier to reason about purely functional specificaion.
> 
> I am sure there is much else to look at and think about, but comments on the above would already be a good start.
> 
> Best regards,
> Karthik
> 
> 
> 
> 
> 
> _______________________________________________
> Hacspec mailing list
> Hacspec at moderncrypto.org <mailto:Hacspec at moderncrypto.org>
> https://moderncrypto.org/mailman/listinfo/hacspec <https://moderncrypto.org/mailman/listinfo/hacspec>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/hacspec/attachments/20180210/a747c940/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <http://moderncrypto.org/mail-archive/hacspec/attachments/20180210/a747c940/attachment-0001.sig>