[hacspec] hacspec syntax

[Ben Laurie]

On 11 February 2018 at 19:21, Franziskus Kiefer <franziskuskiefer at gmail.com>
wrote:

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

Seems a bit simplistic?


>
>
>
>
> 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/20180212/79a3fb86/attachment-0001.html>