[hacspec] hacspec syntax

[Ben Laurie]

On 10 February 2018 at 17:41, Karthikeyan Bhargavan <
karthik.bhargavan at gmail.com> wrote:

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

If it has to be true, we should have a way to express it?

Pre- and post- conditions?


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

Zipping with an explanation is fine.


>
>
> 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
>> https://moderncrypto.org/mailman/listinfo/hacspec
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/hacspec/attachments/20180210/45d31c52/attachment.html>