[hacspec] hacspec syntax

[Franziskus Kiefer]

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

Having pre/post conditions would be great and maybe easier to do.
We could write simple decorators in speclib for pre and post conditions.
I added a simple precondition to chacha20 [1] checking that the counter is
positive. The precondition decorator is implemented in speclib [2].
This is not great yet, but could be a way to add pre- and post-conditions.

Cheers,
Franziskus

[1]
https://github.com/HACS-workshop/hacspec/blob/master/specs/chacha20.py#L59
[2]
https://github.com/HACS-workshop/hacspec/blob/master/specs/speclib.py#L302



On Sat, Feb 10, 2018 at 9:15 PM, Ben Laurie <benl at google.com> wrote:

>
>
> 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
>>
>>
>>
>
> _______________________________________________
> 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/20180211/6d4fa2cf/attachment-0001.html>